clarified options;

--- a/src/Tools/VSCode/etc/options	Wed Dec 28 17:26:38 2016 +0100
+++ b/src/Tools/VSCode/etc/options	Wed Dec 28 17:35:12 2016 +0100
@@ -1,5 +1,11 @@
 (* :mode=isabelle-options: *)
 
+option vscode_input_delay : real = 0.3
+  -- "delay for client input (edits)"
+
+option vscode_output_delay : real = 0.5
+  -- "delay for client output (rendering)"
+
 option vscode_tooltip_margin : int = 60
   -- "margin for pretty-printing of tooltips"
 

--- 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 =