--- a/NEWS Mon Jan 04 20:42:58 2021 +0100
+++ b/NEWS Mon Jan 04 21:25:40 2021 +0100
@@ -46,6 +46,12 @@
collection and sharing of live data on the ML heap. It also includes
information about the Java Runtime system.
+* Action "full-screen-mode" (shortcut F11 or S+F11) has been modified
+for better approximate window size on macOS and Linux/X11. This is
+particularly important for macOS 11.1 Big Sur, where the native
+full-screen mode is incompatible with Java window management: it puts
+dialog windows into an unusable state (Search, Hypersearch, etc.).
+
* PIDE support for session ROOTS: markup for directories.
* Update to jedit-5.6.0, the latest release. This version works properly
--- a/src/Doc/JEdit/JEdit.thy Mon Jan 04 20:42:58 2021 +0100
+++ b/src/Doc/JEdit/JEdit.thy Mon Jan 04 21:25:40 2021 +0100
@@ -2243,11 +2243,20 @@
\<^bold>\<open>Workaround:\<close> Use suitable version of Linux desktops.
\<^item> \<^bold>\<open>Problem:\<close> Full-screen mode via jEdit action @{action_ref
- "toggle-full-screen"} (default keyboard shortcut \<^verbatim>\<open>F11\<close>) works on Windows,
- but not on macOS or various Linux/X11 window managers.
-
- \<^bold>\<open>Workaround:\<close> Use native full-screen control of the window manager (notably
- on macOS).
+ "toggle-full-screen"} (default keyboard shortcut \<^verbatim>\<open>F11\<close> or \<^verbatim>\<open>S+F11\<close>) works
+ robustly on Windows, but not on macOS or various Linux/X11 window managers.
+ For the latter platforms, it is approximated by educated guesses on the
+ window size (excluding the macOS menu bar).
+
+ \<^bold>\<open>Workaround:\<close> Use native full-screen control of the macOS window manager,
+ unless it is macOS 11.1 (Big Sur).
+
+ \<^item> \<^bold>\<open>Problem:\<close> Native full-screen mode on macOS 11.1 is incompatible with
+ Java window management: it puts dialog windows (Search, Hypersearch, etc.)
+ into an unusable state.
+
+ \<^bold>\<open>Workaround:\<close> use the approximative action @{action_ref
+ "toggle-full-screen"}.
\<^item> \<^bold>\<open>Problem:\<close> Heap space of the JVM may fill up and render the Prover IDE
unresponsive, e.g.\ when editing big Isabelle sessions with many theories.
--- a/src/Tools/jEdit/etc/options Mon Jan 04 20:42:58 2021 +0100
+++ b/src/Tools/jEdit/etc/options Mon Jan 04 21:25:40 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)"
--- a/src/Tools/jEdit/src/actions.xml Mon Jan 04 20:42:58 2021 +0100
+++ b/src/Tools/jEdit/src/actions.xml Mon Jan 04 21:25:40 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>
--- a/src/Tools/jEdit/src/isabelle.scala Mon Jan 04 20:42:58 2021 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Mon Jan 04 21:25:40 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)
--- a/src/Tools/jEdit/src/jEdit.props Mon Jan 04 20:42:58 2021 +0100
+++ b/src/Tools/jEdit/src/jEdit.props Mon Jan 04 21:25:40 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