# HG changeset patch # User wenzelm # Date 1488749899 -3600 # Node ID 4d088fe6185ec2c16442a5568951da50c0fbde4e # Parent 1edb570f5b174c89d62591fced3ad76f11199781 more ambitious timing, to compensate general protocol delays; diff -r 1edb570f5b17 -r 4d088fe6185e src/Tools/VSCode/etc/options --- a/src/Tools/VSCode/etc/options Sun Mar 05 22:32:33 2017 +0100 +++ b/src/Tools/VSCode/etc/options Sun Mar 05 22:38:19 2017 +0100 @@ -1,6 +1,6 @@ (* :mode=isabelle-options: *) -option vscode_input_delay : real = 0.3 +option vscode_input_delay : real = 0.1 -- "delay for client input (edits)" option vscode_output_delay : real = 0.5