# HG changeset patch # User wenzelm # Date 1609791940 -3600 # Node ID 6ba08ec184a15178d092900e0eaa3665602f9a12 # Parent 7ad9f197ca7e961e5993f72a937763bfcc1e361f# Parent d77bb4441250142da072455e4ecd38aeabff600a merged diff -r 7ad9f197ca7e -r 6ba08ec184a1 NEWS --- 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 diff -r 7ad9f197ca7e -r 6ba08ec184a1 src/Doc/JEdit/JEdit.thy --- 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>\Workaround:\ Use suitable version of Linux desktops. \<^item> \<^bold>\Problem:\ Full-screen mode via jEdit action @{action_ref - "toggle-full-screen"} (default keyboard shortcut \<^verbatim>\F11\) works on Windows, - but not on macOS or various Linux/X11 window managers. - - \<^bold>\Workaround:\ Use native full-screen control of the window manager (notably - on macOS). + "toggle-full-screen"} (default keyboard shortcut \<^verbatim>\F11\ or \<^verbatim>\S+F11\) 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>\Workaround:\ Use native full-screen control of the macOS window manager, + unless it is macOS 11.1 (Big Sur). + + \<^item> \<^bold>\Problem:\ 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>\Workaround:\ use the approximative action @{action_ref + "toggle-full-screen"}. \<^item> \<^bold>\Problem:\ Heap space of the JVM may fill up and render the Prover IDE unresponsive, e.g.\ when editing big Isabelle sessions with many theories. diff -r 7ad9f197ca7e -r 6ba08ec184a1 src/Tools/jEdit/etc/options --- 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)" diff -r 7ad9f197ca7e -r 6ba08ec184a1 src/Tools/jEdit/src/actions.xml --- 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); - + isabelle.jedit.Isabelle.toggle_full_screen(view); diff -r 7ad9f197ca7e -r 6ba08ec184a1 src/Tools/jEdit/src/isabelle.scala --- 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) diff -r 7ad9f197ca7e -r 6ba08ec184a1 src/Tools/jEdit/src/jEdit.props --- 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