src/Tools/VSCode/etc/options
author wenzelm
Sun, 05 Mar 2017 22:38:19 +0100
changeset 65123 4d088fe6185e
parent 65107 70b0113fa4ef
child 65137 812c35fbffa8
permissions -rw-r--r--
more ambitious timing, to compensate general protocol delays;

(* :mode=isabelle-options: *)

option vscode_input_delay : real = 0.1
  -- "delay for client input (edits)"

option vscode_output_delay : real = 0.5
  -- "delay for client output (rendering)"

option vscode_load_delay : real = 0.5
  -- "delay for file load operations"

option vscode_tooltip_margin : int = 60
  -- "margin for pretty-printing of tooltips"

option vscode_message_margin : int = 80
  -- "margin for pretty-printing of diagnostic messages"

option vscode_timing_threshold : real = 0.1
  -- "default threshold for timing display (seconds)"

option vscode_unicode_symbols : bool = false
  -- "output Isabelle symbols via Unicode (according to etc/symbols)"