# HG changeset patch
# User wenzelm
# Date 1609790566 -3600
# Node ID bef32cb5d26bd232082ba388806d40c07c22c343
# Parent  32edc2b4e24385e0a9ec063af0b16be7d757b0fd
override existing action, to retain menu item;

diff -r 32edc2b4e243 -r bef32cb5d26b src/Tools/jEdit/etc/options
--- 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)"
 
diff -r 32edc2b4e243 -r bef32cb5d26b src/Tools/jEdit/src/actions.xml
--- a/src/Tools/jEdit/src/actions.xml	Mon Jan 04 19:56:33 2021 +0100
+++ b/src/Tools/jEdit/src/actions.xml	Mon Jan 04 21:02:46 2021 +0100
@@ -67,7 +67,7 @@
 	    isabelle.jedit.Isabelle.newline(textArea);
 	  </CODE>
 	</ACTION>
-	<ACTION NAME="isabelle.toggle-full-screen">
+	<ACTION NAME="toggle-full-screen">
 	  <CODE>
 	    isabelle.jedit.Isabelle.toggle_full_screen(view);
 	  </CODE>
diff -r 32edc2b4e243 -r bef32cb5d26b src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Mon Jan 04 19:56:33 2021 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Mon Jan 04 21:02:46 2021 +0100
@@ -233,7 +233,8 @@
   // see toggleFullScreen() method in jEdit/org/gjt/sp/jedit/View.java
   def toggle_full_screen(view: View)
   {
-    if (Untyped.get[Boolean](view, "fullScreenMode")) view.toggleFullScreen()
+    if (PIDE.options.bool("jedit_toggle_full_screen") ||
+        Untyped.get[Boolean](view, "fullScreenMode")) view.toggleFullScreen()
     else {
       Untyped.set[Boolean](view, "fullScreenMode", true)
       val screen = GUI.screen_size(view)
diff -r 32edc2b4e243 -r bef32cb5d26b src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Mon Jan 04 19:56:33 2021 +0100
+++ b/src/Tools/jEdit/src/jEdit.props	Mon Jan 04 21:02:46 2021 +0100
@@ -258,9 +258,6 @@
 isabelle.toggle-breakpoint.label=Toggle Breakpoint
 isabelle.toggle-continuous-checking.label=Toggle continuous checking
 isabelle.toggle-continuous-checking.shortcut=C+e ENTER
-isabelle.toggle-full-screen.label=Toggle full-screen mode
-isabelle.toggle-full-screen.shortcut=F11
-isabelle.toggle-full-screen.shortcut2=S+F11
 isabelle.toggle-node-required.label=Toggle node required
 isabelle.toggle-node-required.shortcut=C+e SPACE
 isabelle.tooltip.label=Show tooltip
@@ -310,6 +307,7 @@
 sidekick.splitter.location=721
 systrayicon=false
 tip.show=false
+toggle-full-screen.shortcut2=S+F11
 toggle-multi-select.shortcut2=C+NUMBER_SIGN
 toggle-rect-select.shortcut2=A+NUMBER_SIGN
 twoStageSave=false