
diff -r d2ce32c5793a -r eb2463fc4d7b src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Mon Oct 12 17:10:36 2015 +0200
+++ b/src/Doc/System/Sessions.thy	Mon Oct 12 17:11:17 2015 +0200
@@ -171,15 +171,15 @@
 
   \begin{itemize}
 
-  \item @{system_option_def "browser_info"} controls output of HTML
+  \<^item> @{system_option_def "browser_info"} controls output of HTML
   browser info, see also \secref{sec:info}.
 
-  \item @{system_option_def "document"} specifies the document output
+  \<^item> @{system_option_def "document"} specifies the document output
   format, see @{tool document} option @{verbatim "-o"} in
   \secref{sec:tool-document}.  In practice, the most relevant values
   are @{verbatim "document=false"} or @{verbatim "document=pdf"}.
 
-  \item @{system_option_def "document_output"} specifies an
+  \<^item> @{system_option_def "document_output"} specifies an
   alternative directory for generated output of the document
   preparation system; the default is within the @{setting
   "ISABELLE_BROWSER_INFO"} hierarchy as explained in
@@ -187,7 +187,7 @@
   default configuration with output readily available to the author of
   the document.
 
-  \item @{system_option_def "document_variants"} specifies document
+  \<^item> @{system_option_def "document_variants"} specifies document
   variants as a colon-separated list of @{text "name=tags"} entries,
   corresponding to @{tool document} options @{verbatim "-n"} and
   @{verbatim "-t"}.
@@ -203,7 +203,7 @@
   different document root entries, see also
   \secref{sec:tool-document}.
 
-  \item @{system_option_def "threads"} determines the number of worker
+  \<^item> @{system_option_def "threads"} determines the number of worker
   threads for parallel checking of theories and proofs.  The default
   @{text "0"} means that a sensible maximum value is determined by the
   underlying hardware.  For machines with many cores or with
@@ -211,7 +211,7 @@
   command-line or within personal settings or preferences, not within
   a session @{verbatim ROOT}).
 
-  \item @{system_option_def "condition"} specifies a comma-separated
+  \<^item> @{system_option_def "condition"} specifies a comma-separated
   list of process environment variables (or Isabelle settings) that
   are required for the subsequent theories to be processed.
   Conditions are considered ``true'' if the corresponding environment
@@ -222,7 +222,7 @@
   explicitly via some shell prefix @{verbatim "env ISABELLE_FULL_TEST=true"}
   before invoking @{tool build}.
 
-  \item @{system_option_def "timeout"} specifies a real wall-clock
+  \<^item> @{system_option_def "timeout"} specifies a real wall-clock
   timeout (in seconds) for the session as a whole.  The timer is
   controlled outside the ML process by the JVM that runs
   Isabelle/Scala.  Thus it is relatively reliable in canceling
@@ -302,7 +302,8 @@
   ML_OPTIONS="..."
 \end{ttbox}
 
-  \medskip Isabelle sessions are defined via session ROOT files as
+  \<^medskip>
+  Isabelle sessions are defined via session ROOT files as
   described in (\secref{sec:session-root}).  The totality of sessions
   is determined by collecting such specifications from all Isabelle
   component directories (\secref{sec:components}), augmented by more
@@ -317,29 +318,34 @@
   command line options persistent (say within @{verbatim
   "$ISABELLE_HOME_USER/ROOTS"}).
 
-  \medskip The subset of sessions to be managed is determined via
+  \<^medskip>
+  The subset of sessions to be managed is determined via
   individual @{text "SESSIONS"} given as command-line arguments, or
   session groups that are given via one or more options @{verbatim
   "-g"}~@{text "NAME"}.  Option @{verbatim "-a"} selects all sessions.
   The build tool takes session dependencies into account: the set of
   selected sessions is completed by including all ancestors.
 
-  \medskip One or more options @{verbatim "-x"}~@{text NAME} specify
+  \<^medskip>
+  One or more options @{verbatim "-x"}~@{text NAME} specify
   sessions to be excluded. All descendents of excluded sessions are removed
   from the selection as specified above. Option @{verbatim "-X"} is
   analogous to this, but excluded sessions are specified by session group
   membership.
 
-  \medskip Option @{verbatim "-R"} reverses the selection in the sense
+  \<^medskip>
+  Option @{verbatim "-R"} reverses the selection in the sense
   that it refers to its requirements: all ancestor sessions excluding
   the original selection.  This allows to prepare the stage for some
   build process with different options, before running the main build
   itself (without option @{verbatim "-R"}).
 
-  \medskip Option @{verbatim "-D"} is similar to @{verbatim "-d"}, but
+  \<^medskip>
+  Option @{verbatim "-D"} is similar to @{verbatim "-d"}, but
   selects all sessions that are defined in the given directories.
 
-  \medskip The build process depends on additional options
+  \<^medskip>
+  The build process depends on additional options
   (\secref{sec:system-options}) that are passed to the prover
   eventually.  The settings variable @{setting_ref
   ISABELLE_BUILD_OPTIONS} allows to provide additional defaults, e.g.\
@@ -351,35 +357,42 @@
   Boolean options.  Multiple occurrences of @{verbatim "-o"} on the
   command-line are applied in the given order.
 
-  \medskip Option @{verbatim "-b"} ensures that heap images are
+  \<^medskip>
+  Option @{verbatim "-b"} ensures that heap images are
   produced for all selected sessions.  By default, images are only
   saved for inner nodes of the hierarchy of sessions, as required for
   other sessions to continue later on.
 
-  \medskip Option @{verbatim "-c"} cleans all descendants of the
+  \<^medskip>
+  Option @{verbatim "-c"} cleans all descendants of the
   selected sessions before performing the specified build operation.
 
-  \medskip Option @{verbatim "-n"} omits the actual build process
+  \<^medskip>
+  Option @{verbatim "-n"} omits the actual build process
   after the preparatory stage (including optional cleanup).  Note that
   the return code always indicates the status of the set of selected
   sessions.
 
-  \medskip Option @{verbatim "-j"} specifies the maximum number of
+  \<^medskip>
+  Option @{verbatim "-j"} specifies the maximum number of
   parallel build jobs (prover processes).  Each prover process is
   subject to a separate limit of parallel worker threads, cf.\ system
   option @{system_option_ref threads}.
 
-  \medskip Option @{verbatim "-s"} enables \emph{system mode}, which
+  \<^medskip>
+  Option @{verbatim "-s"} enables \emph{system mode}, which
   means that resulting heap images and log files are stored in
   @{file_unchecked "$ISABELLE_HOME/heaps"} instead of the default location
   @{setting ISABELLE_OUTPUT} (which is normally in @{setting
   ISABELLE_HOME_USER}, i.e.\ the user's home directory).
 
-  \medskip Option @{verbatim "-v"} increases the general level of
+  \<^medskip>
+  Option @{verbatim "-v"} increases the general level of
   verbosity.  Option @{verbatim "-l"} lists the source files that
   contribute to a session.
 
-  \medskip Option @{verbatim "-k"} specifies a newly proposed keyword for
+  \<^medskip>
+  Option @{verbatim "-k"} 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.\<close>
@@ -393,48 +406,56 @@
 isabelle build -b HOLCF
 \end{ttbox}
 
-  \smallskip Build the main group of logic images:
+  \<^smallskip>
+  Build the main group of logic images:
 \begin{ttbox}
 isabelle build -b -g main
 \end{ttbox}
 
-  \smallskip Provide a general overview of the status of all Isabelle
+  \<^smallskip>
+  Provide a general overview of the status of all Isabelle
   sessions, without building anything:
 \begin{ttbox}
 isabelle build -a -n -v
 \end{ttbox}
 
-  \smallskip Build all sessions with HTML browser info and PDF
+  \<^smallskip>
+  Build all sessions with HTML browser info and PDF
   document preparation:
 \begin{ttbox}
 isabelle build -a -o browser_info -o document=pdf
 \end{ttbox}
 
-  \smallskip Build all sessions with a maximum of 8 parallel prover
+  \<^smallskip>
+  Build all sessions with a maximum of 8 parallel prover
   processes and 4 worker threads each (on a machine with many cores):
 \begin{ttbox}
 isabelle build -a -j8 -o threads=4
 \end{ttbox}
 
-  \smallskip Build some session images with cleanup of their
+  \<^smallskip>
+  Build some session images with cleanup of their
   descendants, while retaining their ancestry:
 \begin{ttbox}
 isabelle build -b -c HOL-Algebra HOL-Word
 \end{ttbox}
 
-  \smallskip Clean all sessions without building anything:
+  \<^smallskip>
+  Clean all sessions without building anything:
 \begin{ttbox}
 isabelle build -a -n -c
 \end{ttbox}
 
-  \smallskip Build all sessions from some other directory hierarchy,
+  \<^smallskip>
+  Build all sessions from some other directory hierarchy,
   according to the settings variable @{verbatim "AFP"} that happens to
   be defined inside the Isabelle environment:
 \begin{ttbox}
 isabelle build -D '$AFP'
 \end{ttbox}
 
-  \smallskip Inform about the status of all sessions required for AFP,
+  \<^smallskip>
+  Inform about the status of all sessions required for AFP,
   without building anything yet:
 \begin{ttbox}
 isabelle build -D '$AFP' -R -v -n




