author | wenzelm |
Wed, 28 Dec 2016 16:45:00 +0100 | |
changeset 64679 | b2bf280b7e13 |
parent 64622 | 529bbb8977c7 |
child 64684 | fe2c9c215b36 |
permissions | -rw-r--r-- |
(* :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)"