--- a/src/Doc/JEdit/JEdit.thy Sun Dec 13 13:16:07 2020 +0100
+++ b/src/Doc/JEdit/JEdit.thy Sun Dec 13 13:29:04 2020 +0100
@@ -49,7 +49,7 @@
experts. Technically, Isabelle/jEdit consists of the original jEdit code
base with minimal patches and a special plugin for Isabelle. This is
integrated as a desktop application for the main operating system
- families: Linux, Windows, Mac OS X.
+ families: Linux, Windows, macOS.
End-users of Isabelle download and run a standalone application that exposes
jEdit as a text editor on the surface. Thus there is occasionally a tendency
@@ -98,7 +98,7 @@
underlines, hyperlinks, popup windows, icons, clickable output etc.
Using the mouse together with the modifier key \<^verbatim>\<open>CONTROL\<close> (Linux, Windows)
- or \<^verbatim>\<open>COMMAND\<close> (Mac OS X) exposes formal content via tooltips and/or
+ or \<^verbatim>\<open>COMMAND\<close> (macOS) exposes formal content via tooltips and/or
hyperlinks (see also \secref{sec:tooltips-hyperlinks}). Output (in popups
etc.) may be explored recursively, using the same techniques as in the
editor source buffer.
@@ -219,7 +219,7 @@
text \<open>
Isabelle/jEdit is normally invoked as a single-instance desktop application,
- based on platform-specific executables for Linux, Windows, Mac OS X.
+ based on platform-specific executables for Linux, Windows, macOS.
It is also possible to invoke the Prover IDE on the command-line, with some
extra options and environment settings. The command-line usage of @{tool_def
@@ -338,7 +338,7 @@
\<^descr>[Windows:] Regular \<^emph>\<open>Windows\<close> is used by default.
- \<^descr>[Mac OS X:] Regular \<^emph>\<open>Mac OS X\<close> is used by default.
+ \<^descr>[macOS:] Regular \<^emph>\<open>Mac OS X\<close> is used by default.
The bundled \<^emph>\<open>MacOSX\<close> plugin provides various functions that are expected
from applications on that particular platform: quit from menu or dock,
@@ -1241,7 +1241,7 @@
text \<open>
Formally processed text (prover input or output) contains rich markup that
can be explored by using the \<^verbatim>\<open>CONTROL\<close> modifier key on Linux and Windows,
- or \<^verbatim>\<open>COMMAND\<close> on Mac OS X. Hovering with the mouse while the modifier is
+ or \<^verbatim>\<open>COMMAND\<close> on macOS. Hovering with the mouse while the modifier is
pressed reveals a \<^emph>\<open>tooltip\<close> (grey box over the text with a yellow popup)
and/or a \<^emph>\<open>hyperlink\<close> (black rectangle over the text with change of mouse
pointer); see also \figref{fig:tooltip}.
@@ -2178,14 +2178,14 @@
\<^bold>\<open>Workaround:\<close> Rebind keys via \<^emph>\<open>Global Options~/ Shortcuts\<close>.
- \<^item> \<^bold>\<open>Problem:\<close> The Mac OS X key sequence \<^verbatim>\<open>COMMAND+COMMA\<close> for application
+ \<^item> \<^bold>\<open>Problem:\<close> The macOS key sequence \<^verbatim>\<open>COMMAND+COMMA\<close> for application
\<^emph>\<open>Preferences\<close> is in conflict with the jEdit default keyboard shortcut for
\<^emph>\<open>Incremental Search Bar\<close> (action @{action_ref "quick-search"}).
\<^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 Mac OS X with native Apple look-and-feel, some exotic
+ \<^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
corresponding jEdit action.
@@ -2193,12 +2193,12 @@
\<^bold>\<open>Workaround:\<close> Disable the native Apple menu bar via Java runtime option
\<^verbatim>\<open>-Dapple.laf.useScreenMenuBar=false\<close>.
- \<^item> \<^bold>\<open>Problem:\<close> Mac OS X system fonts sometimes lead to character drop-outs in
+ \<^item> \<^bold>\<open>Problem:\<close> macOS system fonts sometimes lead to character drop-outs in
the main text area.
\<^bold>\<open>Workaround:\<close> Use the default \<^verbatim>\<open>Isabelle DejaVu\<close> fonts.
- \<^item> \<^bold>\<open>Problem:\<close> On Mac OS X the Java printer dialog sometimes does not work.
+ \<^item> \<^bold>\<open>Problem:\<close> On macOS the Java printer dialog sometimes does not work.
\<^bold>\<open>Workaround:\<close> Use action @{action isabelle.draft} and print via the Web
browser.
@@ -2241,10 +2241,10 @@
\<^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 Mac OS X or various Linux/X11 window managers.
+ 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 Mac OS X).
+ on macOS).
\<^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/Pure/Admin/isabelle_cronjob.scala Sun Dec 13 13:16:07 2020 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala Sun Dec 13 13:29:04 2020 +0100
@@ -237,7 +237,7 @@
" -e ISABELLE_SWIPL=swipl",
args = "-N -a -d '~~/src/Benchmarks'",
detect = Build_Log.Prop.build_tags + " = " + SQL.string("Benchmarks")),
- Remote_Build("Mac OS X 10.14 Mojave (Old)", "lapnipkow3",
+ Remote_Build("macOS 10.14 Mojave (Old)", "lapnipkow3",
options = "-m32 -M1,2 -e ISABELLE_GHC_SETUP=true -p pide_session=false",
self_update = true, args = "-a -d '~~/src/Benchmarks'"),
Remote_Build("AFP old bulky", "lrzcloud1", self_update = true,
@@ -264,19 +264,19 @@
detect =
Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre1") + " OR " +
Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre2")),
- Remote_Build("Poly/ML 5.7 Mac OS X", "macbroy2",
+ Remote_Build("Poly/ML 5.7 macOS", "macbroy2",
history_base = "37074e22e8be",
options = "-m32 -B -M1x4,4 -t polyml-5.7 -i 'init_component /home/isabelle/contrib/polyml-5.7'",
args = "-a",
detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7")),
- Remote_Build("Poly/ML 5.7.1 Mac OS X", "macbroy2",
+ Remote_Build("Poly/ML 5.7.1 macOS", "macbroy2",
history_base = "a9d5b59c3e12",
options = "-m32 -B -M1x4,4 -t polyml-5.7.1-pre2 -i 'init_component /home/isabelle/contrib/polyml-test-905dae2ebfda'",
args = "-a",
detect =
Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre1") + " OR " +
Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre2")),
- Remote_Build("Mac OS X", "macbroy2",
+ Remote_Build("macOS", "macbroy2",
options = "-m32 -M8" +
" -e ISABELLE_GHC=ghc -e ISABELLE_MLTON=mlton -e ISABELLE_OCAML=ocaml" +
" -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
@@ -286,11 +286,11 @@
args = "-a",
detect = Build_Log.Prop.build_tags.undefined,
history_base = "2c0f24e927dd"),
- Remote_Build("Mac OS X, quick_and_dirty", "macbroy2",
+ Remote_Build("macOS, quick_and_dirty", "macbroy2",
options = "-m32 -M8 -t quick_and_dirty -p pide_session=false", args = "-a -o quick_and_dirty",
detect = Build_Log.Prop.build_tags + " = " + SQL.string("quick_and_dirty"),
history_base = "2c0f24e927dd"),
- Remote_Build("Mac OS X, skip_proofs", "macbroy2",
+ Remote_Build("macOS, skip_proofs", "macbroy2",
options = "-m32 -M8 -t skip_proofs -p pide_session=false", args = "-a -o skip_proofs",
detect = Build_Log.Prop.build_tags + " = " + SQL.string("skip_proofs"),
history_base = "2c0f24e927dd"),
@@ -298,10 +298,10 @@
options = "-m32 -B -M1x2,2 -t polyml-test -i 'init_component /home/isabelle/contrib/polyml-5.7-20170217'",
args = "-N -g timing",
detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-test")),
- Remote_Build("Mac OS X 10.12 Sierra", "macbroy30", options = "-m32 -M2 -p pide_session=false", args = "-a",
+ Remote_Build("macOS 10.12 Sierra", "macbroy30", options = "-m32 -M2 -p pide_session=false", args = "-a",
detect = Build_Log.Prop.build_start + " > date '2017-03-03'"),
- Remote_Build("Mac OS X 10.10 Yosemite", "macbroy31", options = "-m32 -M2 -p pide_session=false", args = "-a"),
- Remote_Build("Mac OS X 10.8 Mountain Lion", "macbroy30", options = "-m32 -M2", args = "-a",
+ Remote_Build("macOS 10.10 Yosemite", "macbroy31", options = "-m32 -M2 -p pide_session=false", args = "-a"),
+ Remote_Build("macOS 10.8 Mountain Lion", "macbroy30", options = "-m32 -M2", args = "-a",
detect = Build_Log.Prop.build_start + " < date '2017-03-03'")) :::
{
for { (n, hosts) <- List(1 -> List("lxbroy6"), 2 -> List("lxbroy8", "lxbroy5")) }
@@ -323,11 +323,11 @@
List(
List(Remote_Build("Linux B", "lxbroy10", historic = true, history = 90,
options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")),
- List(Remote_Build("Mac OS X 10.13 High Sierra", "lapbroy68",
+ List(Remote_Build("macOS 10.13 High Sierra", "lapbroy68",
options = "-m32 -B -M1,2,4 -e ISABELLE_GHC_SETUP=true -p pide_session=false",
self_update = true, args = "-a -d '~~/src/Benchmarks'")),
List(
- Remote_Build("Mac OS X 10.14 Mojave", "mini2",
+ Remote_Build("macOS 10.14 Mojave", "mini2",
options = "-m32 -B -M1x2,2,4 -p pide_session=false" +
" -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
" -e ISABELLE_GHC_SETUP=true" +
@@ -335,14 +335,14 @@
" -e ISABELLE_SMLNJ=/usr/local/smlnj/bin/sml" +
" -e ISABELLE_SWIPL=/usr/local/bin/swipl",
self_update = true, args = "-a -d '~~/src/Benchmarks'"),
- Remote_Build("Mac OS X, quick_and_dirty", "mini2",
+ Remote_Build("macOS, quick_and_dirty", "mini2",
options = "-m32 -M4 -t quick_and_dirty -p pide_session=false",
self_update = true, args = "-a -o quick_and_dirty",
detect = Build_Log.Prop.build_tags + " = " + SQL.string("quick_and_dirty")),
- Remote_Build("Mac OS X, skip_proofs", "mini2",
+ Remote_Build("macOS, skip_proofs", "mini2",
options = "-m32 -M4 -t skip_proofs -p pide_session=false", args = "-a -o skip_proofs",
detect = Build_Log.Prop.build_tags + " = " + SQL.string("skip_proofs"))),
- List(Remote_Build("Mac OS X 10.15 Catalina", "laramac01", user = "makarius",
+ List(Remote_Build("macOS 10.15 Catalina", "laramac01", user = "makarius",
proxy_host = "laraserver", proxy_user = "makarius",
self_update = true,
options = "-m32 -M4 -e ISABELLE_GHC_SETUP=true -p pide_session=false",