src/Tools/VSCode/etc/options
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)"