src/Tools/VSCode/src/server.scala

--- a/src/Tools/VSCode/src/server.scala	Wed Dec 28 17:26:38 2016 +0100
+++ b/src/Tools/VSCode/src/server.scala	Wed Dec 28 17:35:12 2016 +0100
@@ -118,7 +118,7 @@
   /* input from client */
 
   private val delay_input =
-    Standard_Thread.delay_last(options.seconds("editor_input_delay")) {
+    Standard_Thread.delay_last(options.seconds("vscode_input_delay")) {
       state.change(st =>
         {
           val changed = (for { entry <- st.models.iterator if entry._2.changed } yield entry).toList
@@ -151,7 +151,7 @@
     }
 
   private val delay_output =
-    Standard_Thread.delay_last(options.seconds("editor_update_delay")) {
+    Standard_Thread.delay_last(options.seconds("vscode_output_delay")) {
       state.change(st =>
         {
           val changed_iterator =