some minor formatting updates

2020-04-09 00:43:25 +02:00
parent 882ea1bc2a
commit a90ff78349
21 changed files with 1954 additions and 1701 deletions
--- a/book/editor.js
+++ b/book/editor.js
@@ -6,12 +6,14 @@ window.editors = [];
    }

    Array.from(document.querySelectorAll('.editable')).forEach(function(editable) {
+        let display_line_numbers = window.playpen_line_numbers || false;
+
        let editor = ace.edit(editable);
            editor.setOptions({
            highlightActiveLine: false,
            showPrintMargin: false,
-            showLineNumbers: false,
-            showGutter: false,
+            showLineNumbers: display_line_numbers,
+            showGutter: display_line_numbers,
            maxLines: Infinity,
            fontSize: "0.875em" // please adjust the font size of the code in general.css
        });