src/Tools/VSCode/etc/options
author wenzelm
Wed, 28 Dec 2016 16:45:00 +0100
changeset 64679 b2bf280b7e13
parent 64622 529bbb8977c7
child 64684 fe2c9c215b36
permissions -rw-r--r--
more uniform treatment of input/output wrt. client; support for diagnistic messages; misc tuning;

(* :mode=isabelle-options: *)

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

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

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