# HG changeset patch
# User wenzelm
# Date 1482942912 -3600
# Node ID fe2c9c215b36f07096e8481fbe980f2fe3b3b188
# Parent  c0c09b6dfbe0dfe9a82a73bd9b8863ccb7c77ee9
clarified options;

diff -r c0c09b6dfbe0 -r fe2c9c215b36 src/Tools/VSCode/etc/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"
 
diff -r c0c09b6dfbe0 -r fe2c9c215b36 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 =