src/Tools/jEdit/etc/options

--- a/src/Tools/jEdit/etc/options	Mon Dec 14 16:51:12 2020 +0100
+++ b/src/Tools/jEdit/etc/options	Mon Dec 14 22:01:54 2020 +0100
@@ -39,6 +39,9 @@
 public option jedit_text_overview : bool = true
   -- "paint text overview column"
 
+public option jedit_focus_modifier : string = "CS"
+  -- "keyboard modifier to enable entity focus regardless of def visibility"
+
 public option isabelle_fonts_hinted : bool = true
   -- "use hinted Isabelle DejaVu fonts (change requires restart)"