--- a/NEWS Sun Jan 10 13:04:29 2021 +0100
+++ b/NEWS Sun Jan 10 13:17:27 2021 +0100
@@ -52,17 +52,17 @@
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
on macOS by default, without the special MacOSX plugin.
+* On macOS Big Sur full-screen mode works requires to change "System
+Preferences / General / Prefer tabs: in full screen" to never.
+
+* Action "full-screen-mode" (shortcut F11 or S+F11) has been modified
+for better approximate window size on macOS and Linux/X11.
+
*** Document preparation ***
--- a/src/Doc/JEdit/JEdit.thy Sun Jan 10 13:04:29 2021 +0100
+++ b/src/Doc/JEdit/JEdit.thy Sun Jan 10 13:17:27 2021 +0100
@@ -2188,6 +2188,13 @@
\<^bold>\<open>Workaround:\<close> Rebind key via \<^emph>\<open>Global Options~/ Shortcuts\<close> according to the
national keyboard layout, e.g.\ \<^verbatim>\<open>COMMAND+SLASH\<close> on English ones.
+ \<^item> \<^bold>\<open>Problem:\<close> On macOS Big Sur full-screen mode causes problems with dialog windows
+ (e.g. \<^emph>\<open>Search and Replace\<close> or \<^emph>\<open>Hypersearch Results\<close>).
+
+ \<^bold>\<open>Workaround:\<close> Go to \<^emph>\<open>System Preferences / General\<close> and change the default
+ ``\<^emph>\<open>Prefer tabs: \<^bold>\<open>in full screen\<close> when opening documents\<close>'' to
+ ``\<^emph>\<open>\<^bold>\<open>never\<close>\<close>''.
+
\<^item> \<^bold>\<open>Problem:\<close> On macOS with native Apple look-and-feel, some exotic
national keyboards may cause a conflict of menu accelerator keys with
regular jEdit key bindings. This leads to duplicate execution of the