equal
deleted
inserted
replaced
21 option vscode_pide_extensions : bool = false |
21 option vscode_pide_extensions : bool = false |
22 -- "use PIDE extensions for Language Server Protocol" |
22 -- "use PIDE extensions for Language Server Protocol" |
23 |
23 |
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 |
|
27 option vscode_caret_perspective : int = 50 |
|
28 -- "number of visible lines above and below the caret (0: unrestricted)" |