equal
deleted
inserted
replaced
24 option vscode_unicode_symbols : bool = false |
24 option vscode_unicode_symbols : bool = false |
25 -- "output Isabelle symbols via Unicode (according to etc/symbols)" |
25 -- "output Isabelle symbols via Unicode (according to etc/symbols)" |
26 |
26 |
27 option vscode_caret_perspective : int = 50 |
27 option vscode_caret_perspective : int = 50 |
28 -- "number of visible lines above and below the caret (0: unrestricted)" |
28 -- "number of visible lines above and below the caret (0: unrestricted)" |
|
29 |
|
30 option vscode_caret_preview : bool = false |
|
31 -- "dynamic preview of caret document node" |