| author | wenzelm |
| Wed, 28 Dec 2016 17:35:12 +0100 | |
| changeset 64684 | fe2c9c215b36 |
| parent 64679 | b2bf280b7e13 |
| child 64727 | 13e37567a0d6 |
| permissions | -rw-r--r-- |
|
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
1 |
(* :mode=isabelle-options: *) |
|
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
2 |
|
| 64684 | 3 |
option vscode_input_delay : real = 0.3 |
4 |
-- "delay for client input (edits)" |
|
5 |
||
6 |
option vscode_output_delay : real = 0.5 |
|
7 |
-- "delay for client output (rendering)" |
|
8 |
||
|
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
9 |
option vscode_tooltip_margin : int = 60 |
|
64679
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64622
diff
changeset
|
10 |
-- "margin for pretty-printing of tooltips" |
|
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64622
diff
changeset
|
11 |
|
|
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64622
diff
changeset
|
12 |
option vscode_diagnostics_margin : int = 80 |
|
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64622
diff
changeset
|
13 |
-- "margin for pretty-printing of diagnostic messages" |
|
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
14 |
|
|
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
15 |
option vscode_timing_threshold : real = 0.1 |
|
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
16 |
-- "default threshold for timing display (seconds)" |