# HG changeset patch
# User wenzelm
# Date 1609791855 -3600
# Node ID d77bb4441250142da072455e4ecd38aeabff600a
# Parent  bef32cb5d26bd232082ba388806d40c07c22c343
more documentation;

diff -r bef32cb5d26b -r d77bb4441250 NEWS
--- a/NEWS	Mon Jan 04 21:02:46 2021 +0100
+++ b/NEWS	Mon Jan 04 21:24:15 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
diff -r bef32cb5d26b -r d77bb4441250 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Mon Jan 04 21:02:46 2021 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Mon Jan 04 21:24:15 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.