--- a/src/Tools/jEdit/etc/options Mon Jan 04 19:56:33 2021 +0100
+++ b/src/Tools/jEdit/etc/options Mon Jan 04 21:02:46 2021 +0100
@@ -42,6 +42,9 @@
public option jedit_focus_modifier : string = "CS"
-- "keyboard modifier to enable entity focus regardless of def visibility"
+public option jedit_toggle_full_screen : bool = false
+ -- "use original jEdit action toggle-full-screen instead of Isabelle/jEdit variant"
+
public option isabelle_fonts_hinted : bool = true
-- "use hinted Isabelle DejaVu fonts (change requires restart)"