src/Doc/System/Sessions.thy

   patterns\<close> specifies theory exports that may get written to the file-system,
   e.g. via @{tool_ref build} with option \<^verbatim>\<open>-e\<close> (\secref{sec:tool-build}). The
   \<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>
 
 
 subsubsection \<open>Examples\<close>
 

 
     \<^item> @{system_option_def "document_echo"} informs about document file names
     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
     tell {\LaTeX} how to interpret certain Isabelle command regions:
     ``\<^verbatim>\<open>+\<close>\<open>foo\<close>'' (or just ``\<open>foo\<close>'') means to keep, ``\<^verbatim>\<open>-\<close>\<open>foo\<close>'' to drop,

     \<^verbatim>\<open>\isamarkupsection\<close>.
 
     \<^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>).
 
     \<^item> @{system_option_def "condition"} specifies a comma-separated list of
     process environment variables (or Isabelle settings) that are required for

 
   \<^medskip>
   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>
   Option \<^verbatim>\<open>-b\<close> ensures that heap images are produced for all selected
   sessions. By default, images are only saved for inner nodes of the hierarchy

   \<^medskip>
   Option \<^verbatim>\<open>-N\<close> enables cyclic shuffling of NUMA CPU nodes. This may help
   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.
-
-  \<^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>-v\<close> increases the general level of verbosity.
+
+  \<^medskip>
+  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>
 
 
 subsubsection \<open>Examples\<close>
 

   database, notably via @{system_option system_heaps}, or @{system_option
   build_database_server} and its relatives.
 
   \<^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
   per line (76 + 4 characters to prefix warnings or errors).
 

     -d DIR       include session directory
     -l           list exports
     -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.
 
   The PATTERN language resembles glob patterns in the shell, with ? and *

     -a           select all sessions
     -b NAME      base logic image (default "Pure")
     -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
 
   Update theory sources based on PIDE markup.\<close>}
 

   \<^medskip> Option \<^verbatim>\<open>-o\<close> overrides Isabelle system options as for @{tool build}
   (\secref{sec:tool-build}). Option \<^verbatim>\<open>-u\<close> refers to specific \<^verbatim>\<open>update\<close>
   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
     or atomic identifiers. For example, ``\<^theory_text>\<open>lemma \<doublequote>x =
     x\<doublequote>\<close>'' is replaced by ``\<^theory_text>\<open>lemma \<open>x = x\<close>\<close>'', and ``\<^theory_text>\<open>assume

   \<^verbatim>\<open>HOL-Analysis\<close> (and ancestors):
 
   @{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>}
 
   \<^smallskip> Update sessions that build on \<^verbatim>\<open>HOL-Proofs\<close>, which need to be run
   separately with special options as follows: