changeset 65926 | 0f7821a07aa9 |
parent 65137 | 812c35fbffa8 |
child 65977 | c51b74be23b6 |
--- a/src/Tools/VSCode/etc/options Thu May 25 19:50:37 2017 +0200 +++ b/src/Tools/VSCode/etc/options Thu May 25 21:20:22 2017 +0200 @@ -23,3 +23,6 @@ option vscode_unicode_symbols : bool = false -- "output Isabelle symbols via Unicode (according to etc/symbols)" + +option vscode_caret_perspective : int = 50 + -- "number of visible lines above and below the caret (0: unrestricted)"