# HG changeset patch
# User wenzelm
# Date 1645988423 -3600
# Node ID 95612f330c93f75ee119b20b3301b7fe02fa8968
# Parent  d48998648281edde3d9e7bf7dbb5997840cf7990
misc tuning based on comments by Heiko Eißfeldt;

diff -r d48998648281 -r 95612f330c93 src/Doc/System/Environment.thy
--- 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
diff -r d48998648281 -r 95612f330c93 src/Doc/System/Misc.thy
--- 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>
diff -r d48998648281 -r 95612f330c93 src/Doc/System/Phabricator.thy
--- 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:
 
diff -r d48998648281 -r 95612f330c93 src/Doc/System/Presentation.thy
--- 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>
 
 
diff -r d48998648281 -r 95612f330c93 src/Doc/System/Scala.thy
--- 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
diff -r d48998648281 -r 95612f330c93 src/Doc/System/Server.thy
--- 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>
diff -r d48998648281 -r 95612f330c93 src/Doc/System/Sessions.thy
--- 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>}
 
diff -r d48998648281 -r 95612f330c93 src/Pure/Tools/update.scala
--- 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