[bugfix] monospace font not working on mac os

[bugfix] missing update of internal datastructure in some cases
letmp · Mar 10, 2022 · 244619e · 244619e
1 parent 6a8ff72
commit 244619e
Show file tree

Hide file tree

Showing 7 changed files with 30 additions and 30 deletions.
diff --git a/language-extensions/sublime/droid-lang/buildscript/webapp/droid.html b/language-extensions/sublime/droid-lang/buildscript/webapp/droid.html
@@ -407,7 +407,7 @@
         color: var(--color-export-description);
     }
     .exportContent textarea{ 
-        font-family: 'Consolas';
+        font-family: Consolas, "Andale Mono WT", "Andale Mono", "Lucida Console", "Lucida Sans Typewriter", "DejaVu Sans Mono", "Bitstream Vera Sans Mono", "Liberation Mono", "Nimbus Mono L", Monaco, "Courier New", Courier, monospace;
         display: block; 
         width: 370px;
         border: 1px solid var(--color-border);
@@ -1084,7 +1084,7 @@
   }
 
   // calls a stateUpdate (after a certain amount of time without input updates)
-  submitTextareaInput(action, droidComponentId, registerId, value, timeout = 500){
+  submitTextareaInput(action, droidComponentId, registerId, value, timeout = 300){
     clearTimeout(this.timeout);
     this.timeout = setTimeout(function () {
         window.sh.updateState(action, [droidComponentId, registerId, value])
@@ -1305,7 +1305,7 @@
         textareaDesc.placeholder = "_"
         textareaDesc.textContent = dc.content[0].content
         textareaDesc.addEventListener("input", window.renderer.updateTextareaSize)
-        //textareaDesc.addEventListener('keyup', e => window.renderer.submitTextareaInput("updateDescription",dc.id, dc.content[0].id, textareaDesc.value))
+        textareaDesc.addEventListener('keyup', e => window.renderer.submitTextareaInput("updateDescription",dc.id, dc.content[0].id, textareaDesc.value))
         textareaDesc.addEventListener('blur', e => window.renderer.submitTextareaInput("updateDescription",dc.id, dc.content[0].id, textareaDesc.value, 0))
         divContent.appendChild(textareaDesc)
         divContent.appendChild(document.createElement("br"))
@@ -1339,7 +1339,7 @@
           textareaVar.addEventListener("input", function () {this.value = this.value.toUpperCase(); });
           textareaVar.textContent = register.variablename
           setTimeout(function () {window.renderer.initTextareaSize(textareaVar)}, 10);
-          //textareaVar.addEventListener('keyup', e => window.renderer.submitTextareaInput("updateVariable",dc.id, register.id, textareaVar.value))
+          textareaVar.addEventListener('keyup', e => window.renderer.submitTextareaInput("updateVariable",dc.id, register.id, textareaVar.value))
           textareaVar.addEventListener('blur', e => window.renderer.submitTextareaInput("updateVariable",dc.id, register.id, textareaVar.value, 0))
           var textareaDesc = document.createElement("textarea")
           textareaDesc.classList.add('varDescription')
@@ -1348,7 +1348,7 @@
           textareaDesc.addEventListener("input", window.renderer.updateTextareaSize)
           textareaDesc.textContent = register.description
           setTimeout(function () {window.renderer.initTextareaSize(textareaDesc)}, 10);
-          //textareaDesc.addEventListener('keyup', e => window.renderer.submitTextareaInput("updateDescription",dc.id, register.id, textareaDesc.value))
+          textareaDesc.addEventListener('keyup', e => window.renderer.submitTextareaInput("updateDescription",dc.id, register.id, textareaDesc.value))
           textareaDesc.addEventListener('blur', e => window.renderer.submitTextareaInput("updateDescription",dc.id, register.id, textareaDesc.value, 0))
           var div1 = document.createElement("div")
             var div11 = document.createElement("div")

diff --git a/language-extensions/sublime/droid.html b/language-extensions/sublime/droid.html
@@ -407,7 +407,7 @@
         color: var(--color-export-description);
     }
     .exportContent textarea{ 
-        font-family: 'Consolas';
+        font-family: Consolas, "Andale Mono WT", "Andale Mono", "Lucida Console", "Lucida Sans Typewriter", "DejaVu Sans Mono", "Bitstream Vera Sans Mono", "Liberation Mono", "Nimbus Mono L", Monaco, "Courier New", Courier, monospace;
         display: block; 
         width: 370px;
         border: 1px solid var(--color-border);
@@ -1084,7 +1084,7 @@
   }
 
   // calls a stateUpdate (after a certain amount of time without input updates)
-  submitTextareaInput(action, droidComponentId, registerId, value, timeout = 500){
+  submitTextareaInput(action, droidComponentId, registerId, value, timeout = 300){
     clearTimeout(this.timeout);
     this.timeout = setTimeout(function () {
         window.sh.updateState(action, [droidComponentId, registerId, value])
@@ -1305,7 +1305,7 @@
         textareaDesc.placeholder = "_"
         textareaDesc.textContent = dc.content[0].content
         textareaDesc.addEventListener("input", window.renderer.updateTextareaSize)
-        //textareaDesc.addEventListener('keyup', e => window.renderer.submitTextareaInput("updateDescription",dc.id, dc.content[0].id, textareaDesc.value))
+        textareaDesc.addEventListener('keyup', e => window.renderer.submitTextareaInput("updateDescription",dc.id, dc.content[0].id, textareaDesc.value))
         textareaDesc.addEventListener('blur', e => window.renderer.submitTextareaInput("updateDescription",dc.id, dc.content[0].id, textareaDesc.value, 0))
         divContent.appendChild(textareaDesc)
         divContent.appendChild(document.createElement("br"))
@@ -1339,7 +1339,7 @@
           textareaVar.addEventListener("input", function () {this.value = this.value.toUpperCase(); });
           textareaVar.textContent = register.variablename
           setTimeout(function () {window.renderer.initTextareaSize(textareaVar)}, 10);
-          //textareaVar.addEventListener('keyup', e => window.renderer.submitTextareaInput("updateVariable",dc.id, register.id, textareaVar.value))
+          textareaVar.addEventListener('keyup', e => window.renderer.submitTextareaInput("updateVariable",dc.id, register.id, textareaVar.value))
           textareaVar.addEventListener('blur', e => window.renderer.submitTextareaInput("updateVariable",dc.id, register.id, textareaVar.value, 0))
           var textareaDesc = document.createElement("textarea")
           textareaDesc.classList.add('varDescription')
@@ -1348,7 +1348,7 @@
           textareaDesc.addEventListener("input", window.renderer.updateTextareaSize)
           textareaDesc.textContent = register.description
           setTimeout(function () {window.renderer.initTextareaSize(textareaDesc)}, 10);
-          //textareaDesc.addEventListener('keyup', e => window.renderer.submitTextareaInput("updateDescription",dc.id, register.id, textareaDesc.value))
+          textareaDesc.addEventListener('keyup', e => window.renderer.submitTextareaInput("updateDescription",dc.id, register.id, textareaDesc.value))
           textareaDesc.addEventListener('blur', e => window.renderer.submitTextareaInput("updateDescription",dc.id, register.id, textareaDesc.value, 0))
           var div1 = document.createElement("div")
             var div11 = document.createElement("div")

diff --git a/language-extensions/vscode/droid-lang/buildscript/webapp/droid.html b/language-extensions/vscode/droid-lang/buildscript/webapp/droid.html
@@ -407,7 +407,7 @@
         color: var(--color-export-description);
     }
     .exportContent textarea{ 
-        font-family: 'Consolas';
+        font-family: Consolas, "Andale Mono WT", "Andale Mono", "Lucida Console", "Lucida Sans Typewriter", "DejaVu Sans Mono", "Bitstream Vera Sans Mono", "Liberation Mono", "Nimbus Mono L", Monaco, "Courier New", Courier, monospace;
         display: block; 
         width: 370px;
         border: 1px solid var(--color-border);
@@ -1084,7 +1084,7 @@
   }
 
   // calls a stateUpdate (after a certain amount of time without input updates)
-  submitTextareaInput(action, droidComponentId, registerId, value, timeout = 500){
+  submitTextareaInput(action, droidComponentId, registerId, value, timeout = 300){
     clearTimeout(this.timeout);
     this.timeout = setTimeout(function () {
         window.sh.updateState(action, [droidComponentId, registerId, value])
@@ -1305,7 +1305,7 @@
         textareaDesc.placeholder = "_"
         textareaDesc.textContent = dc.content[0].content
         textareaDesc.addEventListener("input", window.renderer.updateTextareaSize)
-        //textareaDesc.addEventListener('keyup', e => window.renderer.submitTextareaInput("updateDescription",dc.id, dc.content[0].id, textareaDesc.value))
+        textareaDesc.addEventListener('keyup', e => window.renderer.submitTextareaInput("updateDescription",dc.id, dc.content[0].id, textareaDesc.value))
         textareaDesc.addEventListener('blur', e => window.renderer.submitTextareaInput("updateDescription",dc.id, dc.content[0].id, textareaDesc.value, 0))
         divContent.appendChild(textareaDesc)
         divContent.appendChild(document.createElement("br"))
@@ -1339,7 +1339,7 @@
           textareaVar.addEventListener("input", function () {this.value = this.value.toUpperCase(); });
           textareaVar.textContent = register.variablename
           setTimeout(function () {window.renderer.initTextareaSize(textareaVar)}, 10);
-          //textareaVar.addEventListener('keyup', e => window.renderer.submitTextareaInput("updateVariable",dc.id, register.id, textareaVar.value))
+          textareaVar.addEventListener('keyup', e => window.renderer.submitTextareaInput("updateVariable",dc.id, register.id, textareaVar.value))
           textareaVar.addEventListener('blur', e => window.renderer.submitTextareaInput("updateVariable",dc.id, register.id, textareaVar.value, 0))
           var textareaDesc = document.createElement("textarea")
           textareaDesc.classList.add('varDescription')
@@ -1348,7 +1348,7 @@
           textareaDesc.addEventListener("input", window.renderer.updateTextareaSize)
           textareaDesc.textContent = register.description
           setTimeout(function () {window.renderer.initTextareaSize(textareaDesc)}, 10);
-          //textareaDesc.addEventListener('keyup', e => window.renderer.submitTextareaInput("updateDescription",dc.id, register.id, textareaDesc.value))
+          textareaDesc.addEventListener('keyup', e => window.renderer.submitTextareaInput("updateDescription",dc.id, register.id, textareaDesc.value))
           textareaDesc.addEventListener('blur', e => window.renderer.submitTextareaInput("updateDescription",dc.id, register.id, textareaDesc.value, 0))
           var div1 = document.createElement("div")
             var div11 = document.createElement("div")

diff --git a/language-extensions/vscode/droid.html b/language-extensions/vscode/droid.html
@@ -407,7 +407,7 @@
         color: var(--color-export-description);
     }
     .exportContent textarea{ 
-        font-family: 'Consolas';
+        font-family: Consolas, "Andale Mono WT", "Andale Mono", "Lucida Console", "Lucida Sans Typewriter", "DejaVu Sans Mono", "Bitstream Vera Sans Mono", "Liberation Mono", "Nimbus Mono L", Monaco, "Courier New", Courier, monospace;
         display: block; 
         width: 370px;
         border: 1px solid var(--color-border);
@@ -1084,7 +1084,7 @@
   }
 
   // calls a stateUpdate (after a certain amount of time without input updates)
-  submitTextareaInput(action, droidComponentId, registerId, value, timeout = 500){
+  submitTextareaInput(action, droidComponentId, registerId, value, timeout = 300){
     clearTimeout(this.timeout);
     this.timeout = setTimeout(function () {
         window.sh.updateState(action, [droidComponentId, registerId, value])
@@ -1305,7 +1305,7 @@
         textareaDesc.placeholder = "_"
         textareaDesc.textContent = dc.content[0].content
         textareaDesc.addEventListener("input", window.renderer.updateTextareaSize)
-        //textareaDesc.addEventListener('keyup', e => window.renderer.submitTextareaInput("updateDescription",dc.id, dc.content[0].id, textareaDesc.value))
+        textareaDesc.addEventListener('keyup', e => window.renderer.submitTextareaInput("updateDescription",dc.id, dc.content[0].id, textareaDesc.value))
         textareaDesc.addEventListener('blur', e => window.renderer.submitTextareaInput("updateDescription",dc.id, dc.content[0].id, textareaDesc.value, 0))
         divContent.appendChild(textareaDesc)
         divContent.appendChild(document.createElement("br"))
@@ -1339,7 +1339,7 @@
           textareaVar.addEventListener("input", function () {this.value = this.value.toUpperCase(); });
           textareaVar.textContent = register.variablename
           setTimeout(function () {window.renderer.initTextareaSize(textareaVar)}, 10);
-          //textareaVar.addEventListener('keyup', e => window.renderer.submitTextareaInput("updateVariable",dc.id, register.id, textareaVar.value))
+          textareaVar.addEventListener('keyup', e => window.renderer.submitTextareaInput("updateVariable",dc.id, register.id, textareaVar.value))
           textareaVar.addEventListener('blur', e => window.renderer.submitTextareaInput("updateVariable",dc.id, register.id, textareaVar.value, 0))
           var textareaDesc = document.createElement("textarea")
           textareaDesc.classList.add('varDescription')
@@ -1348,7 +1348,7 @@
           textareaDesc.addEventListener("input", window.renderer.updateTextareaSize)
           textareaDesc.textContent = register.description
           setTimeout(function () {window.renderer.initTextareaSize(textareaDesc)}, 10);
-          //textareaDesc.addEventListener('keyup', e => window.renderer.submitTextareaInput("updateDescription",dc.id, register.id, textareaDesc.value))
+          textareaDesc.addEventListener('keyup', e => window.renderer.submitTextareaInput("updateDescription",dc.id, register.id, textareaDesc.value))
           textareaDesc.addEventListener('blur', e => window.renderer.submitTextareaInput("updateDescription",dc.id, register.id, textareaDesc.value, 0))
           var div1 = document.createElement("div")
             var div11 = document.createElement("div")

diff --git a/webapp/droid.html b/webapp/droid.html
@@ -407,7 +407,7 @@
         color: var(--color-export-description);
     }
     .exportContent textarea{ 
-        font-family: 'Consolas';
+        font-family: Consolas, "Andale Mono WT", "Andale Mono", "Lucida Console", "Lucida Sans Typewriter", "DejaVu Sans Mono", "Bitstream Vera Sans Mono", "Liberation Mono", "Nimbus Mono L", Monaco, "Courier New", Courier, monospace;
         display: block; 
         width: 370px;
         border: 1px solid var(--color-border);
@@ -1084,7 +1084,7 @@
   }
 
   // calls a stateUpdate (after a certain amount of time without input updates)
-  submitTextareaInput(action, droidComponentId, registerId, value, timeout = 500){
+  submitTextareaInput(action, droidComponentId, registerId, value, timeout = 300){
     clearTimeout(this.timeout);
     this.timeout = setTimeout(function () {
         window.sh.updateState(action, [droidComponentId, registerId, value])
@@ -1305,7 +1305,7 @@
         textareaDesc.placeholder = "_"
         textareaDesc.textContent = dc.content[0].content
         textareaDesc.addEventListener("input", window.renderer.updateTextareaSize)
-        //textareaDesc.addEventListener('keyup', e => window.renderer.submitTextareaInput("updateDescription",dc.id, dc.content[0].id, textareaDesc.value))
+        textareaDesc.addEventListener('keyup', e => window.renderer.submitTextareaInput("updateDescription",dc.id, dc.content[0].id, textareaDesc.value))
         textareaDesc.addEventListener('blur', e => window.renderer.submitTextareaInput("updateDescription",dc.id, dc.content[0].id, textareaDesc.value, 0))
         divContent.appendChild(textareaDesc)
         divContent.appendChild(document.createElement("br"))
@@ -1339,7 +1339,7 @@
           textareaVar.addEventListener("input", function () {this.value = this.value.toUpperCase(); });
           textareaVar.textContent = register.variablename
           setTimeout(function () {window.renderer.initTextareaSize(textareaVar)}, 10);
-          //textareaVar.addEventListener('keyup', e => window.renderer.submitTextareaInput("updateVariable",dc.id, register.id, textareaVar.value))
+          textareaVar.addEventListener('keyup', e => window.renderer.submitTextareaInput("updateVariable",dc.id, register.id, textareaVar.value))
           textareaVar.addEventListener('blur', e => window.renderer.submitTextareaInput("updateVariable",dc.id, register.id, textareaVar.value, 0))
           var textareaDesc = document.createElement("textarea")
           textareaDesc.classList.add('varDescription')
@@ -1348,7 +1348,7 @@
           textareaDesc.addEventListener("input", window.renderer.updateTextareaSize)
           textareaDesc.textContent = register.description
           setTimeout(function () {window.renderer.initTextareaSize(textareaDesc)}, 10);
-          //textareaDesc.addEventListener('keyup', e => window.renderer.submitTextareaInput("updateDescription",dc.id, register.id, textareaDesc.value))
+          textareaDesc.addEventListener('keyup', e => window.renderer.submitTextareaInput("updateDescription",dc.id, register.id, textareaDesc.value))
           textareaDesc.addEventListener('blur', e => window.renderer.submitTextareaInput("updateDescription",dc.id, register.id, textareaDesc.value, 0))
           var div1 = document.createElement("div")
             var div11 = document.createElement("div")

diff --git a/webapp/src/droid.css b/webapp/src/droid.css
@@ -383,7 +383,7 @@
         color: var(--color-export-description);
     }
     .exportContent textarea{ 
-        font-family: 'Consolas';
+        font-family: Consolas, "Andale Mono WT", "Andale Mono", "Lucida Console", "Lucida Sans Typewriter", "DejaVu Sans Mono", "Bitstream Vera Sans Mono", "Liberation Mono", "Nimbus Mono L", Monaco, "Courier New", Courier, monospace;
         display: block; 
         width: 370px;
         border: 1px solid var(--color-border);

diff --git a/webapp/src/droid.js b/webapp/src/droid.js
@@ -623,7 +623,7 @@ class Renderer {
   }
 
   // calls a stateUpdate (after a certain amount of time without input updates)
-  submitTextareaInput(action, droidComponentId, registerId, value, timeout = 500){
+  submitTextareaInput(action, droidComponentId, registerId, value, timeout = 300){
     clearTimeout(this.timeout);
     this.timeout = setTimeout(function () {
         window.sh.updateState(action, [droidComponentId, registerId, value])
@@ -844,7 +844,7 @@ class Renderer {
         textareaDesc.placeholder = "_"
         textareaDesc.textContent = dc.content[0].content
         textareaDesc.addEventListener("input", window.renderer.updateTextareaSize)
-        //textareaDesc.addEventListener('keyup', e => window.renderer.submitTextareaInput("updateDescription",dc.id, dc.content[0].id, textareaDesc.value))
+        textareaDesc.addEventListener('keyup', e => window.renderer.submitTextareaInput("updateDescription",dc.id, dc.content[0].id, textareaDesc.value))
         textareaDesc.addEventListener('blur', e => window.renderer.submitTextareaInput("updateDescription",dc.id, dc.content[0].id, textareaDesc.value, 0))
         divContent.appendChild(textareaDesc)
         divContent.appendChild(document.createElement("br"))
@@ -878,7 +878,7 @@ class Renderer {
           textareaVar.addEventListener("input", function () {this.value = this.value.toUpperCase(); });
           textareaVar.textContent = register.variablename
           setTimeout(function () {window.renderer.initTextareaSize(textareaVar)}, 10);
-          //textareaVar.addEventListener('keyup', e => window.renderer.submitTextareaInput("updateVariable",dc.id, register.id, textareaVar.value))
+          textareaVar.addEventListener('keyup', e => window.renderer.submitTextareaInput("updateVariable",dc.id, register.id, textareaVar.value))
           textareaVar.addEventListener('blur', e => window.renderer.submitTextareaInput("updateVariable",dc.id, register.id, textareaVar.value, 0))
           var textareaDesc = document.createElement("textarea")
           textareaDesc.classList.add('varDescription')
@@ -887,7 +887,7 @@ class Renderer {
           textareaDesc.addEventListener("input", window.renderer.updateTextareaSize)
           textareaDesc.textContent = register.description
           setTimeout(function () {window.renderer.initTextareaSize(textareaDesc)}, 10);
-          //textareaDesc.addEventListener('keyup', e => window.renderer.submitTextareaInput("updateDescription",dc.id, register.id, textareaDesc.value))
+          textareaDesc.addEventListener('keyup', e => window.renderer.submitTextareaInput("updateDescription",dc.id, register.id, textareaDesc.value))
           textareaDesc.addEventListener('blur', e => window.renderer.submitTextareaInput("updateDescription",dc.id, register.id, textareaDesc.value, 0))
           var div1 = document.createElement("div")
             var div11 = document.createElement("div")