| author | wenzelm |
| Wed, 12 Mar 2025 11:39:00 +0100 | |
| changeset 82265 | 4b875a4c83b0 |
| parent 81084 | 96eb20106a34 |
| 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 |
|
|
81049
45ef41e823f7
added vscode options tag;
Thomas Lindae <thomas.lindae@in.tum.de>
parents:
81024
diff
changeset
|
3 |
option vscode_input_delay : real = 0.1 for vscode |
| 64684 | 4 |
-- "delay for client input (edits)" |
5 |
||
|
81049
45ef41e823f7
added vscode options tag;
Thomas Lindae <thomas.lindae@in.tum.de>
parents:
81024
diff
changeset
|
6 |
option vscode_output_delay : real = 0.5 for vscode |
| 64684 | 7 |
-- "delay for client output (rendering)" |
8 |
||
|
81049
45ef41e823f7
added vscode options tag;
Thomas Lindae <thomas.lindae@in.tum.de>
parents:
81024
diff
changeset
|
9 |
option vscode_load_delay : real = 0.5 for vscode |
|
64727
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 |
|
|
81049
45ef41e823f7
added vscode options tag;
Thomas Lindae <thomas.lindae@in.tum.de>
parents:
81024
diff
changeset
|
12 |
option vscode_tooltip_margin : int = 60 for vscode |
|
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 |
|
|
81049
45ef41e823f7
added vscode options tag;
Thomas Lindae <thomas.lindae@in.tum.de>
parents:
81024
diff
changeset
|
15 |
option vscode_message_margin : int = 80 for vscode |
|
64679
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 |
|
|
81049
45ef41e823f7
added vscode options tag;
Thomas Lindae <thomas.lindae@in.tum.de>
parents:
81024
diff
changeset
|
18 |
option vscode_timing_threshold : real = 0.1 for vscode |
|
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
19 |
-- "default threshold for timing display (seconds)" |
| 64870 | 20 |
|
|
81049
45ef41e823f7
added vscode options tag;
Thomas Lindae <thomas.lindae@in.tum.de>
parents:
81024
diff
changeset
|
21 |
option vscode_pide_extensions : bool = false for vscode |
| 65137 | 22 |
-- "use PIDE extensions for Language Server Protocol" |
23 |
||
|
81062
b2df8bf17071
lsp: created distinction for unicode symbols setting between output and edits and clarified output text functions;
Thomas Lindae <thomas.lindae@in.tum.de>
parents:
81049
diff
changeset
|
24 |
option vscode_unicode_symbols_output : bool = false for vscode |
| 81084 | 25 |
-- "output Isabelle symbols via Unicode in Output (according to etc/symbols)" |
|
81062
b2df8bf17071
lsp: created distinction for unicode symbols setting between output and edits and clarified output text functions;
Thomas Lindae <thomas.lindae@in.tum.de>
parents:
81049
diff
changeset
|
26 |
|
|
b2df8bf17071
lsp: created distinction for unicode symbols setting between output and edits and clarified output text functions;
Thomas Lindae <thomas.lindae@in.tum.de>
parents:
81049
diff
changeset
|
27 |
option vscode_unicode_symbols_edits : bool = false for vscode |
| 81084 | 28 |
-- "output Isabelle symbols via Unicode in Edits (according to etc/symbols)" |
|
65926
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65137
diff
changeset
|
29 |
|
|
81049
45ef41e823f7
added vscode options tag;
Thomas Lindae <thomas.lindae@in.tum.de>
parents:
81024
diff
changeset
|
30 |
option vscode_caret_perspective : int = 50 for vscode |
|
65926
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65137
diff
changeset
|
31 |
-- "number of visible lines above and below the caret (0: unrestricted)" |
|
65977
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
65926
diff
changeset
|
32 |
|
|
81049
45ef41e823f7
added vscode options tag;
Thomas Lindae <thomas.lindae@in.tum.de>
parents:
81024
diff
changeset
|
33 |
option vscode_caret_preview : bool = false for vscode |
|
65977
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
65926
diff
changeset
|
34 |
-- "dynamic preview of caret document node" |
|
81024
d1535ba3b1ca
lsp: added vscode_html_output option;
Thomas Lindae <thomas.lindae@in.tum.de>
parents:
65977
diff
changeset
|
35 |
|
|
81049
45ef41e823f7
added vscode options tag;
Thomas Lindae <thomas.lindae@in.tum.de>
parents:
81024
diff
changeset
|
36 |
option vscode_html_output : bool = false for vscode |
|
81024
d1535ba3b1ca
lsp: added vscode_html_output option;
Thomas Lindae <thomas.lindae@in.tum.de>
parents:
65977
diff
changeset
|
37 |
-- "output State and Output in HTML" |