| author | wenzelm |
| Sat, 31 Dec 2016 20:26:34 +0100 | |
| changeset 64727 | 13e37567a0d6 |
| parent 64684 | fe2c9c215b36 |
| child 64870 | 41e2797af496 |
| 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 |
||
|
64727
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64684
diff
changeset
|
9 |
option vscode_load_delay : real = 0.5 |
|
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64684
diff
changeset
|
10 |
-- "delay for file load operations" |
|
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64684
diff
changeset
|
11 |
|
|
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
12 |
option vscode_tooltip_margin : int = 60 |
|
64679
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64622
diff
changeset
|
13 |
-- "margin for pretty-printing of tooltips" |
|
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64622
diff
changeset
|
14 |
|
|
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64622
diff
changeset
|
15 |
option vscode_diagnostics_margin : int = 80 |
|
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64622
diff
changeset
|
16 |
-- "margin for pretty-printing of diagnostic messages" |
|
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
17 |
|
|
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
18 |
option vscode_timing_threshold : real = 0.1 |
|
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
19 |
-- "default threshold for timing display (seconds)" |