--- a/src/Doc/System/Environment.thy Sun Feb 27 18:58:50 2022 +0100
+++ b/src/Doc/System/Environment.thy Sun Feb 27 20:00:23 2022 +0100
@@ -23,8 +23,8 @@
process environment. This is a statically scoped collection of environment
variables, such as @{setting ISABELLE_HOME}, @{setting ML_SYSTEM}, @{setting
ML_HOME}. These variables are \<^emph>\<open>not\<close> intended to be set directly from the
- shell, but are provided by Isabelle \<^emph>\<open>components\<close> their \<^emph>\<open>settings files\<close> as
- explained below.
+ shell, but are provided by Isabelle \<^emph>\<open>components\<close> within their \<^emph>\<open>settings
+ files\<close>, as explained below.
\<close>
@@ -286,7 +286,7 @@
ISABELLE_TOOLS} settings variable (colon-separated list in standard POSIX
notation).
- \<^enum> If a file ``\<open>tool\<close>\<^verbatim>\<open>.scala\<close>'' is found, the source needs to define
+ \<^enum> If a file ``\<open>tool\<close>\<^verbatim>\<open>.scala\<close>'' is found, the content needs to define
some object that extends the class \<^verbatim>\<open>Isabelle_Tool.Body\<close>. The Scala
compiler is invoked on the spot (which may take some time), and the body
function is run with the command-line arguments as \<^verbatim>\<open>List[String]\<close>.
@@ -347,7 +347,7 @@
Options \<^verbatim>\<open>-e\<close> and \<^verbatim>\<open>-f\<close> allow to evaluate ML code, before the ML process is
started. The source is either given literally or taken from a file. Multiple
\<^verbatim>\<open>-e\<close> and \<^verbatim>\<open>-f\<close> options are evaluated in the given order. Errors lead to
- premature exit of the ML process with return code 1.
+ a premature exit of the ML process with return code 1.
\<^medskip>
Option \<^verbatim>\<open>-T\<close> loads a specified theory file. This is a wrapper for \<^verbatim>\<open>-e\<close> with
--- a/src/Doc/System/Misc.thy Sun Feb 27 18:58:50 2022 +0100
+++ b/src/Doc/System/Misc.thy Sun Feb 27 20:00:23 2022 +0100
@@ -170,7 +170,7 @@
\<^medskip>
Options \<^verbatim>\<open>-u\<close> and \<^verbatim>\<open>-x\<close> operate on user components listed in
- \<^path>\<open>$ISABELLE_HOME_USER/etc/components\<close>: this avoid manual editing if
+ \<^path>\<open>$ISABELLE_HOME_USER/etc/components\<close>: this avoids manual editing of
Isabelle configuration files.
\<close>
@@ -281,7 +281,7 @@
The local \<^verbatim>\<open>.hg/hgrc\<close> file is changed to refer to the remote repository,
usually via the symbolic path name ``\<^verbatim>\<open>default\<close>''; option \<^verbatim>\<open>-p\<close> allows to
- provided a different name.
+ provide a different name.
\<close>
subsubsection \<open>Examples\<close>
--- a/src/Doc/System/Phabricator.thy Sun Feb 27 18:58:50 2022 +0100
+++ b/src/Doc/System/Phabricator.thy Sun Feb 27 20:00:23 2022 +0100
@@ -160,7 +160,7 @@
@{verbatim [display] \<open> isabelle phabricator_setup_mail\<close>}
- \<^noindent> This generates a JSON template file for the the mail account details.
+ \<^noindent> This generates a JSON template file for the mail account details.
After editing that, the subsequent command will add and test it with
Phabricator:
--- a/src/Doc/System/Presentation.thy Sun Feb 27 18:58:50 2022 +0100
+++ b/src/Doc/System/Presentation.thy Sun Feb 27 20:00:23 2022 +0100
@@ -43,8 +43,8 @@
@{tool build} with suitable options:
@{verbatim [display] \<open>isabelle build -o browser_info -v -c FOL\<close>}
- The presentation output will appear in \<^verbatim>\<open>$ISABELLE_BROWSER_INFO/FOL/FOL\<close> as
- reported by the above verbose invocation of the build process.
+ The presentation output will appear in a sub-directory
+ \<^path>\<open>$ISABELLE_BROWSER_INFO\<close>, according to the chapter and session name.
Many Isabelle sessions (such as \<^session>\<open>HOL-Library\<close> in
\<^dir>\<open>~~/src/HOL/Library\<close>) also provide theory documents in PDF. These are
@@ -57,11 +57,11 @@
\secref{sec:tool-document} for further details.
\<^bigskip>
- The theory browsing information is stored in a sub-directory directory
- determined by the @{setting_ref ISABELLE_BROWSER_INFO} setting plus a prefix
- corresponding to the session chapter and identifier. In order to present
- Isabelle applications on the web, the corresponding subdirectory from
- @{setting ISABELLE_BROWSER_INFO} can be put on a WWW server.
+ The theory browsing information is stored in the directory determined by the
+ @{setting_ref ISABELLE_BROWSER_INFO} setting, with sub-directory structure
+ according to the chapter and session name. In order to present Isabelle
+ applications on the web, the corresponding subdirectory from @{setting
+ ISABELLE_BROWSER_INFO} can be put on a WWW server.
\<close>
--- a/src/Doc/System/Scala.thy Sun Feb 27 18:58:50 2022 +0100
+++ b/src/Doc/System/Scala.thy Sun Feb 27 20:00:23 2022 +0100
@@ -151,7 +151,7 @@
also possible to invoke @{tool scala_build} explicitly, with extra options.
\<^medskip>
- The syntax of in \<^path>\<open>etc/build.props\<close> follows a regular Java properties
+ The syntax of \<^path>\<open>etc/build.props\<close> follows a regular Java properties
file\<^footnote>\<open>\<^url>\<open>https://docs.oracle.com/en/java/javase/15/docs/api/java.base/java/util/Properties.html#load(java.io.Reader)\<close>\<close>,
but the encoding is \<^verbatim>\<open>UTF-8\<close>, instead of historic \<^verbatim>\<open>ISO 8859-1\<close> from the API
documentation.
@@ -193,7 +193,7 @@
\<^file>\<open>$ISABELLE_HOME/lib/classes/isabelle.jar\<close> (especially relevant for
add-on modules).
- A \<^emph>\<open>special entry\<close> is of of the form \<^verbatim>\<open>env:\<close>\<open>variable\<close> and refers to a
+ A \<^emph>\<open>special entry\<close> is of the form \<^verbatim>\<open>env:\<close>\<open>variable\<close> and refers to a
settings variable from the Isabelle environment: its value may consist of
multiple \<^verbatim>\<open>jar\<close> entries (separated by colons). Environment variables are
not expanded recursively.
@@ -334,7 +334,7 @@
The service class \<^scala_type>\<open>isabelle.Scala.Functions\<close> collects Scala
functions of type \<^scala_type>\<open>isabelle.Scala.Fun\<close>: by registering
instances via \<^verbatim>\<open>services\<close> in \<^path>\<open>etc/build.props\<close>
- (\secref{sec:scala-build}), it is becomes possible to invoke Isabelle/Scala
+ (\secref{sec:scala-build}), it becomes possible to invoke Isabelle/Scala
from Isabelle/ML (see below).
An example is the predefined collection of
@@ -382,7 +382,7 @@
interrupts within the ML runtime environment as usual. A \<^scala>\<open>null\<close>
result in Scala raises an exception \<^ML>\<open>Scala.Null\<close> in ML. The execution
of \<open>@{scala}\<close> works via a Scala future on a bounded thread farm, while
- \<open>@{scala_thread}\<close> always forks a separate Java thread.
+ \<open>@{scala_thread}\<close> always forks a separate Java/VM thread.
The standard approach of representing datatypes via strings works via XML in
YXML transfer syntax. See Isabelle/ML operations and modules @{ML
--- a/src/Doc/System/Server.thy Sun Feb 27 18:58:50 2022 +0100
+++ b/src/Doc/System/Server.thy Sun Feb 27 20:00:23 2022 +0100
@@ -16,9 +16,9 @@
In contrast, the Isabelle server exposes Isabelle/Scala as a
``terminate-stay-resident'' application that manages multiple logic
- \<^emph>\<open>sessions\<close> and concurrent tasks to use \<^emph>\<open>theories\<close>. This provides an
- analogous to \<^ML>\<open>Thy_Info.use_theories\<close> in Isabelle/ML, but with full
- concurrency and Isabelle/PIDE markup.
+ \<^emph>\<open>sessions\<close> and concurrent tasks to use \<^emph>\<open>theories\<close>. This is analogous to
+ \<^ML>\<open>Thy_Info.use_theories\<close> in Isabelle/ML, with proper support for
+ concurrent invocations.
The client/server arrangement via TCP sockets also opens possibilities for
remote Isabelle services that are accessed by local applications, e.g.\ via
@@ -197,7 +197,7 @@
arbitrary bytes excluding CR (13) and LF (10), and terminated by CR-LF or
just LF.
- \<^item> A \<^emph>\<open>long message\<close> starts with a single that consists only of decimal
+ \<^item> A \<^emph>\<open>long message\<close> starts with a single line consisting of decimal
digits: these are interpreted as length of the subsequent block of
arbitrary bytes. A final line-terminator (as above) may be included here,
but is not required.
@@ -227,9 +227,8 @@
subsection \<open>Input and output messages \label{sec:input-output-messages}\<close>
text \<open>
- Server input and output messages have a uniform format as follows:
-
- \<^item> \<open>name argument\<close> such that:
+ The uniform format for server input and output messages is \<open>name argument\<close>,
+ such that:
\<^item> \<open>name\<close> is the longest prefix consisting of ASCII letters, digits,
``\<^verbatim>\<open>_\<close>'', ``\<^verbatim>\<open>.\<close>'',
@@ -262,7 +261,7 @@
\<^item> JSON value (Scala type \<^verbatim>\<open>JSON.T\<close>)
JSON values may consist of objects (records), arrays (lists), strings,
- numbers, bools, null.\<^footnote>\<open>See also the official specification
+ numbers, bools, or null.\<^footnote>\<open>See also the official specification
\<^url>\<open>https://www.json.org\<close> and unofficial explorations ``Parsing JSON is a
Minefield'' \<^url>\<open>http://seriot.ch/parsing_json.php\<close>.\<close> Since JSON requires
explicit quotes and backslash-escapes to represent arbitrary text, the YXML
@@ -820,7 +819,7 @@
text \<open>
The \<open>session_id\<close> provides the internal identification of the session object
- within the sever process. It can remain active as long as the server is
+ within the server process. It can remain active as long as the server is
running, independently of the current client connection.
\<^medskip>
--- a/src/Doc/System/Sessions.thy Sun Feb 27 18:58:50 2022 +0100
+++ b/src/Doc/System/Sessions.thy Sun Feb 27 20:00:23 2022 +0100
@@ -170,9 +170,9 @@
\<open>target_dir\<close> specification is relative to the session root directory; its
default is \<^verbatim>\<open>export\<close>. Exports are selected via \<open>patterns\<close> as in @{tool_ref
export} (\secref{sec:tool-export}). The number given in brackets (default:
- 0) specifies elements that should be pruned from each name: it allows to
- reduce the resulting directory hierarchy at the danger of overwriting files
- due to loss of uniqueness.
+ 0) specifies the prefix of elements that should be removed from each name:
+ it allows to reduce the resulting directory hierarchy at the danger of
+ overwriting files due to loss of uniqueness.
\<close>
@@ -216,7 +216,7 @@
during session presentation.
\<^item> @{system_option_def "document_variants"} specifies document variants as
- a colon-separated list of \<open>name=tags\<close> entries. The default name
+ a colon-separated list of \<open>name=tags\<close> entries. The default name is
\<^verbatim>\<open>document\<close>, without additional tags.
Tags are specified as a comma separated list of modifier/name pairs and
@@ -260,7 +260,7 @@
\<^item> @{system_option_def "threads"} determines the number of worker threads
for parallel checking of theories and proofs. The default \<open>0\<close> means that a
sensible maximum value is determined by the underlying hardware. For
- machines with many cores or with hyperthreading, this is often requires
+ machines with many cores or with hyperthreading, this sometimes requires
manual adjustment (on the command-line or within personal settings or
preferences, not within a session \<^verbatim>\<open>ROOT\<close>).
@@ -431,7 +431,7 @@
Option \<^verbatim>\<open>-P\<close> enables PDF/HTML presentation in the given directory, where
``\<^verbatim>\<open>-P:\<close>'' refers to the default @{setting_ref ISABELLE_BROWSER_INFO} (or
@{setting_ref ISABELLE_BROWSER_INFO_SYSTEM}). This applies only to
- explicitly selected sessions; note that option \<open>-R\<close> allows to select all
+ explicitly selected sessions; note that option \<^verbatim>\<open>-R\<close> allows to select all
requirements separately.
\<^medskip>
@@ -471,14 +471,16 @@
performance tuning on Linux servers with separate CPU/memory modules.
\<^medskip>
- Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity. Option \<^verbatim>\<open>-l\<close> lists
- the source files that contribute to a session.
+ Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity.
\<^medskip>
- Option \<^verbatim>\<open>-k\<close> specifies a newly proposed keyword for outer syntax (multiple
- uses allowed). The theory sources are checked for conflicts wrt.\ this
- hypothetical change of syntax, e.g.\ to reveal occurrences of identifiers
- that need to be quoted.
+ Option \<^verbatim>\<open>-l\<close> lists the source files that contribute to a session.
+
+ \<^medskip>
+ Option \<^verbatim>\<open>-k\<close> specifies a newly proposed keyword for outer syntax. It is
+ possible to use option \<^verbatim>\<open>-k\<close> repeatedly to check multiple keywords. The
+ theory sources are checked for conflicts wrt.\ this hypothetical change of
+ syntax, e.g.\ to reveal occurrences of identifiers that need to be quoted.
\<close>
@@ -569,7 +571,7 @@
\<^medskip> Option \<^verbatim>\<open>-T\<close> restricts output to given theories: multiple entries are
possible by repeating this option on the command-line. The default is to
- refer to \<^emph>\<open>all\<close> theories that were used in original session build process.
+ refer to \<^emph>\<open>all\<close> theories used in the original session build process.
\<^medskip> Options \<^verbatim>\<open>-m\<close> and \<^verbatim>\<open>-U\<close> modify pretty printing and output of Isabelle
symbols. The default is for an old-fashioned ASCII terminal at 80 characters
@@ -602,7 +604,7 @@
-n no build of session
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-p NUM prune path of exported files by NUM elements
- -x PATTERN extract files matching pattern (e.g.\ "*:**" for all)
+ -x PATTERN extract files matching pattern (e.g. "*:**" for all)
List or export theory exports for SESSION: named blobs produced by
isabelle build. Option -l or -x is required; option -x may be repeated.
@@ -735,7 +737,7 @@
-d DIR include session directory
-g NAME select session group NAME
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- -u OPT overide update option: shortcut for "-o update_OPT"
+ -u OPT override "update" option: shortcut for "-o update_OPT"
-v verbose
-x NAME exclude session NAME and all descendants
@@ -756,7 +758,7 @@
options, by relying on naming convention: ``\<^verbatim>\<open>-u\<close>~\<open>OPT\<close>'' is a shortcut for
``\<^verbatim>\<open>-o\<close>~\<^verbatim>\<open>update_\<close>\<open>OPT\<close>''.
- \<^medskip> The following update options are supported:
+ \<^medskip> The following \<^verbatim>\<open>update\<close> options are supported:
\<^item> @{system_option update_inner_syntax_cartouches} to update inner syntax
(types, terms, etc.)~to use cartouches, instead of double-quoted strings
@@ -798,7 +800,7 @@
@{verbatim [display] \<open>isabelle update -u mixfix_cartouches HOL-Analysis\<close>}
\<^smallskip> Update the same for all application sessions based on \<^verbatim>\<open>HOL-Analysis\<close> ---
- using its image is taken starting point (for reduced resource requirements):
+ using its image as starting point (for reduced resource requirements):
@{verbatim [display] \<open>isabelle update -u mixfix_cartouches -b HOL-Analysis -B HOL-Analysis\<close>}
--- a/src/Pure/Tools/update.scala Sun Feb 27 18:58:50 2022 +0100
+++ b/src/Pure/Tools/update.scala Sun Feb 27 20:00:23 2022 +0100
@@ -92,7 +92,7 @@
-d DIR include session directory
-g NAME select session group NAME
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- -u OPT overide update option: shortcut for "-o update_OPT"
+ -u OPT override "update" option: shortcut for "-o update_OPT"
-v verbose
-x NAME exclude session NAME and all descendants