editor.js 875 B

1234567891011121314151617181920212223242526272829
  1. "use strict";
  2. window.editors = [];
  3. (function(editors) {
  4. if (typeof(ace) === 'undefined' || !ace) {
  5. return;
  6. }
  7. Array.from(document.querySelectorAll('.editable')).forEach(function(editable) {
  8. let display_line_numbers = window.playground_line_numbers || false;
  9. let editor = ace.edit(editable);
  10. editor.setOptions({
  11. highlightActiveLine: false,
  12. showPrintMargin: false,
  13. showLineNumbers: display_line_numbers,
  14. showGutter: display_line_numbers,
  15. maxLines: Infinity,
  16. fontSize: "0.875em" // please adjust the font size of the code in general.css
  17. });
  18. editor.$blockScrolling = Infinity;
  19. editor.getSession().setMode("ace/mode/rust");
  20. editor.originalCode = editor.getValue();
  21. editors.push(editor);
  22. });
  23. })(window.editors);