From 621db0ff4251eb22e70d64bed79a03eee57445ba Mon Sep 17 00:00:00 2001
From: Silvan Calarco <silvan.calarco@mambasoft.it>
Date: Sun, 28 Jul 2019 20:45:29 +0200
Subject: [PATCH] Fixes after codemirror update

---
 styles/webbuild.css |  2 +-
 webbuild.js.inc     | 10 +++++-----
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/styles/webbuild.css b/styles/webbuild.css
index 1c7c4ff..7c2283f 100644
--- a/styles/webbuild.css
+++ b/styles/webbuild.css
@@ -256,7 +256,7 @@ div#container {
    width:100%;
 }
 .CodeMirror {
-   font-size:9pt;
+   font-size:10pt;
    font-family:monospace;
    line-height:1em;
 }
diff --git a/webbuild.js.inc b/webbuild.js.inc
index 1a4aeb0..6f482eb 100644
--- a/webbuild.js.inc
+++ b/webbuild.js.inc
@@ -96,13 +96,13 @@ function ajax_getvalues(request,confirm) {
           var spectext = document.getElementById("spectext");
           if ((nodes[i].nodeName == "editor") && (spectext != undefined) && (spectext.parentNode != undefined))
               {
-             editor = CodeMirror.fromTextArea(spectext,
-                { lineNumbers: true,
+             editor = CodeMirror.fromTextArea(spectext, {
+                  lineNumbers: false,
                   tabSize: 4,
                   indentUnit: 4,
-                  indentWithTabs: true,
-                  onChange: function() { editorChanged(); }
-                });
+                  indentWithTabs: true
+             });
+             editor.on('change', function() { editorChanged(); });
              editor.setSize(null, 500);
           } else if ((nodes[i].nodeName == "output") && (document.getElementById("outputbottom") != undefined)) {
              document.getElementById("outputbottom").scrollTop = document.getElementById("outputbottom").scrollHeight;