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"