# HG changeset patch
# User wenzelm
# Date 1446664726 -3600
# Node ID f18f6e51e901858bfa2af91c64b83d633e19ae4f
# Parent  e717f152d2a81fa011743790306fae048af0ae2a
tuned whitespace;

diff -r e717f152d2a8 -r f18f6e51e901 src/Doc/System/Basics.thy
--- a/src/Doc/System/Basics.thy	Wed Nov 04 19:52:38 2015 +0100
+++ b/src/Doc/System/Basics.thy	Wed Nov 04 20:18:46 2015 +0100
@@ -1,35 +1,34 @@
+(*:wrap=hard:maxLineLen=78:*)
+
 theory Basics
 imports Base
 begin
 
 chapter \<open>The Isabelle system environment\<close>
 
-text \<open>This manual describes Isabelle together with related tools and
-  user interfaces as seen from a system oriented view.  See also the
-  \<^emph>\<open>Isabelle/Isar Reference Manual\<close> @{cite "isabelle-isar-ref"} for
-  the actual Isabelle input language and related concepts, and
-  \<^emph>\<open>The Isabelle/Isar Implementation
+text \<open>
+  This manual describes Isabelle together with related tools and user
+  interfaces as seen from a system oriented view. See also the \<^emph>\<open>Isabelle/Isar
+  Reference Manual\<close> @{cite "isabelle-isar-ref"} for the actual Isabelle input
+  language and related concepts, and \<^emph>\<open>The Isabelle/Isar Implementation
   Manual\<close> @{cite "isabelle-implementation"} for the main concepts of the
   underlying implementation in Isabelle/ML.
 
   \<^medskip>
-  The Isabelle system environment provides the following
-  basic infrastructure to integrate tools smoothly.
+  The Isabelle system environment provides the following basic infrastructure
+  to integrate tools smoothly.
 
-  \<^enum> The \<^emph>\<open>Isabelle settings\<close> mechanism provides process
-  environment variables to all Isabelle executables (including tools
-  and user interfaces).
+  \<^enum> The \<^emph>\<open>Isabelle settings\<close> mechanism provides process environment variables
+  to all Isabelle executables (including tools and user interfaces).
 
-  \<^enum> The raw \<^emph>\<open>Isabelle process\<close> (@{executable_ref
-  "isabelle_process"}) runs logic sessions either interactively or in
-  batch mode.  In particular, this view abstracts over the invocation
-  of the actual ML system to be used.  Regular users rarely need to
-  care about the low-level process.
+  \<^enum> The raw \<^emph>\<open>Isabelle process\<close> (@{executable_ref "isabelle_process"}) runs
+  logic sessions either interactively or in batch mode. In particular, this
+  view abstracts over the invocation of the actual ML system to be used.
+  Regular users rarely need to care about the low-level process.
 
-  \<^enum> The main \<^emph>\<open>Isabelle tool wrapper\<close> (@{executable_ref
-  isabelle}) provides a generic startup environment Isabelle related
-  utilities, user interfaces etc.  Such tools automatically benefit
-  from the settings mechanism.
+  \<^enum> The main \<^emph>\<open>Isabelle tool wrapper\<close> (@{executable_ref isabelle}) provides a
+  generic startup environment Isabelle related utilities, user interfaces etc.
+  Such tools automatically benefit from the settings mechanism.
 \<close>
 
 
@@ -37,299 +36,270 @@
 
 text \<open>
   The Isabelle system heavily depends on the \<^emph>\<open>settings
-  mechanism\<close>\indexbold{settings}.  Essentially, 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,
-  though.  Isabelle employs a somewhat more sophisticated scheme of
-  \<^emph>\<open>settings files\<close> --- one for site-wide defaults, another for
-  additional user-specific modifications.  With all configuration
-  variables in clearly defined places, this scheme is more
-  maintainable and user-friendly than global shell environment
-  variables.
+  mechanism\<close>\indexbold{settings}. Essentially, 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, though. Isabelle employs a
+  somewhat more sophisticated scheme of \<^emph>\<open>settings files\<close> --- one for
+  site-wide defaults, another for additional user-specific modifications. With
+  all configuration variables in clearly defined places, this scheme is more
+  maintainable and user-friendly than global shell environment variables.
 
-  In particular, we avoid the typical situation where prospective
-  users of a software package are told to put several things into
-  their shell startup scripts, before being able to actually run the
-  program. Isabelle requires none such administrative chores of its
-  end-users --- the executables can be invoked straight away.
-  Occasionally, users would still want to put the @{file
-  "$ISABELLE_HOME/bin"} directory into their shell's search path, but
+  In particular, we avoid the typical situation where prospective users of a
+  software package are told to put several things into their shell startup
+  scripts, before being able to actually run the program. Isabelle requires
+  none such administrative chores of its end-users --- the executables can be
+  invoked straight away. Occasionally, users would still want to put the
+  @{file "$ISABELLE_HOME/bin"} directory into their shell's search path, but
   this is not required.
 \<close>
 
 
 subsection \<open>Bootstrapping the environment \label{sec:boot}\<close>
 
-text \<open>Isabelle executables need to be run within a proper settings
-  environment.  This is bootstrapped as described below, on the first
-  invocation of one of the outer wrapper scripts (such as
-  @{executable_ref isabelle}).  This happens only once for each
-  process tree, i.e.\ the environment is passed to subprocesses
-  according to regular Unix conventions.
+text \<open>
+  Isabelle executables need to be run within a proper settings environment.
+  This is bootstrapped as described below, on the first invocation of one of
+  the outer wrapper scripts (such as @{executable_ref isabelle}). This happens
+  only once for each process tree, i.e.\ the environment is passed to
+  subprocesses according to regular Unix conventions.
+
+    \<^enum> The special variable @{setting_def ISABELLE_HOME} is determined
+    automatically from the location of the binary that has been run.
 
-  \<^enum> The special variable @{setting_def ISABELLE_HOME} is
-  determined automatically from the location of the binary that has
-  been run.
-  
-  You should not try to set @{setting ISABELLE_HOME} manually. Also
-  note that the Isabelle executables either have to be run from their
-  original location in the distribution directory, or via the
-  executable objects created by the @{tool install} tool.  Symbolic
-  links are admissible, but a plain copy of the @{file
-  "$ISABELLE_HOME/bin"} files will not work!
+    You should not try to set @{setting ISABELLE_HOME} manually. Also note
+    that the Isabelle executables either have to be run from their original
+    location in the distribution directory, or via the executable objects
+    created by the @{tool install} tool. Symbolic links are admissible, but a
+    plain copy of the @{file "$ISABELLE_HOME/bin"} files will not work!
+
+    \<^enum> The file @{file "$ISABELLE_HOME/etc/settings"} is run as a
+    @{executable_ref bash} shell script with the auto-export option for
+    variables enabled.
 
-  \<^enum> The file @{file "$ISABELLE_HOME/etc/settings"} is run as a
-  @{executable_ref bash} shell script with the auto-export option for
-  variables enabled.
-  
-  This file holds a rather long list of shell variable assigments,
-  thus providing the site-wide default settings.  The Isabelle
-  distribution already contains a global settings file with sensible
-  defaults for most variables.  When installing the system, only a few
-  of these may have to be adapted (probably @{setting ML_SYSTEM}
-  etc.).
-  
-  \<^enum> The file @{file_unchecked "$ISABELLE_HOME_USER/etc/settings"} (if it
-  exists) is run in the same way as the site default settings. Note
-  that the variable @{setting ISABELLE_HOME_USER} has already been set
-  before --- usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/IsabelleXXXX\<close>.
-  
-  Thus individual users may override the site-wide defaults.
-  Typically, a user settings file contains only a few lines, with some
-  assignments that are actually changed.  Never copy the central
-  @{file "$ISABELLE_HOME/etc/settings"} file!
+    This file holds a rather long list of shell variable assignments, thus
+    providing the site-wide default settings. The Isabelle distribution
+    already contains a global settings file with sensible defaults for most
+    variables. When installing the system, only a few of these may have to be
+    adapted (probably @{setting ML_SYSTEM} etc.).
+
+    \<^enum> The file @{file_unchecked "$ISABELLE_HOME_USER/etc/settings"} (if it
+    exists) is run in the same way as the site default settings. Note that the
+    variable @{setting ISABELLE_HOME_USER} has already been set before ---
+    usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/IsabelleXXXX\<close>.
 
+    Thus individual users may override the site-wide defaults. Typically, a
+    user settings file contains only a few lines, with some assignments that
+    are actually changed. Never copy the central @{file
+    "$ISABELLE_HOME/etc/settings"} file!
 
-  Since settings files are regular GNU @{executable_def bash} scripts,
-  one may use complex shell commands, such as \<^verbatim>\<open>if\<close> or
-  \<^verbatim>\<open>case\<close> statements to set variables depending on the
-  system architecture or other environment variables.  Such advanced
-  features should be added only with great care, though. In
-  particular, external environment references should be kept at a
+  Since settings files are regular GNU @{executable_def bash} scripts, one may
+  use complex shell commands, such as \<^verbatim>\<open>if\<close> or \<^verbatim>\<open>case\<close> statements to set
+  variables depending on the system architecture or other environment
+  variables. Such advanced features should be added only with great care,
+  though. In particular, external environment references should be kept at a
   minimum.
 
   \<^medskip>
   A few variables are somewhat special:
 
-  \<^item> @{setting_def ISABELLE_PROCESS} and @{setting_def ISABELLE_TOOL} are set
-  automatically to the absolute path names of the @{executable
-  "isabelle_process"} and @{executable isabelle} executables,
-  respectively.
-  
-  \<^item> @{setting_ref ISABELLE_OUTPUT} will have the identifiers of
-  the Isabelle distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and
-  the ML system (cf.\ @{setting ML_IDENTIFIER}) appended automatically
-  to its value.
+    \<^item> @{setting_def ISABELLE_PROCESS} and @{setting_def ISABELLE_TOOL} are set
+    automatically to the absolute path names of the @{executable
+    "isabelle_process"} and @{executable isabelle} executables, respectively.
 
+    \<^item> @{setting_ref ISABELLE_OUTPUT} will have the identifiers of the Isabelle
+    distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and the ML system (cf.\
+    @{setting ML_IDENTIFIER}) appended automatically to its value.
 
   \<^medskip>
-  Note that the settings environment may be inspected with
-  the @{tool getenv} tool.  This might help to figure out the effect
-  of complex settings scripts.\<close>
+  Note that the settings environment may be inspected with the @{tool getenv}
+  tool. This might help to figure out the effect of complex settings scripts.
+\<close>
 
 
 subsection \<open>Common variables\<close>
 
 text \<open>
-  This is a reference of common Isabelle settings variables. Note that
-  the list is somewhat open-ended. Third-party utilities or interfaces
-  may add their own selection. Variables that are special in some
-  sense are marked with \<open>\<^sup>*\<close>.
+  This is a reference of common Isabelle settings variables. Note that the
+  list is somewhat open-ended. Third-party utilities or interfaces may add
+  their own selection. Variables that are special in some sense are marked
+  with \<open>\<^sup>*\<close>.
 
-  \<^descr>[@{setting_def USER_HOME}\<open>\<^sup>*\<close>] Is the cross-platform
-  user home directory.  On Unix systems this is usually the same as
-  @{setting HOME}, but on Windows it is the regular home directory of
-  the user, not the one of within the Cygwin root
-  file-system.\<^footnote>\<open>Cygwin itself offers another choice whether
-  its HOME should point to the @{file_unchecked "/home"} directory tree or the
+  \<^descr>[@{setting_def USER_HOME}\<open>\<^sup>*\<close>] Is the cross-platform user home directory.
+  On Unix systems this is usually the same as @{setting HOME}, but on Windows
+  it is the regular home directory of the user, not the one of within the
+  Cygwin root file-system.\<^footnote>\<open>Cygwin itself offers another choice whether its
+  HOME should point to the @{file_unchecked "/home"} directory tree or the
   Windows user home.\<close>
 
-  \<^descr>[@{setting_def ISABELLE_HOME}\<open>\<^sup>*\<close>] is the location of the
-  top-level Isabelle distribution directory. This is automatically
-  determined from the Isabelle executable that has been invoked.  Do
-  not attempt to set @{setting ISABELLE_HOME} yourself from the shell!
-  
-  \<^descr>[@{setting_def ISABELLE_HOME_USER}] is the user-specific
-  counterpart of @{setting ISABELLE_HOME}. The default value is
-  relative to @{file_unchecked "$USER_HOME/.isabelle"}, under rare
-  circumstances this may be changed in the global setting file.
-  Typically, the @{setting ISABELLE_HOME_USER} directory mimics
-  @{setting ISABELLE_HOME} to some extend. In particular, site-wide
-  defaults may be overridden by a private
-  \<^verbatim>\<open>$ISABELLE_HOME_USER/etc/settings\<close>.
+  \<^descr>[@{setting_def ISABELLE_HOME}\<open>\<^sup>*\<close>] is the location of the top-level
+  Isabelle distribution directory. This is automatically determined from the
+  Isabelle executable that has been invoked. Do not attempt to set @{setting
+  ISABELLE_HOME} yourself from the shell!
 
-  \<^descr>[@{setting_def ISABELLE_PLATFORM_FAMILY}\<open>\<^sup>*\<close>] is
-  automatically set to the general platform family: \<^verbatim>\<open>linux\<close>,
-  \<^verbatim>\<open>macos\<close>, \<^verbatim>\<open>windows\<close>.  Note that
+  \<^descr>[@{setting_def ISABELLE_HOME_USER}] is the user-specific counterpart of
+  @{setting ISABELLE_HOME}. The default value is relative to @{file_unchecked
+  "$USER_HOME/.isabelle"}, under rare circumstances this may be changed in the
+  global setting file. Typically, the @{setting ISABELLE_HOME_USER} directory
+  mimics @{setting ISABELLE_HOME} to some extend. In particular, site-wide
+  defaults may be overridden by a private \<^verbatim>\<open>$ISABELLE_HOME_USER/etc/settings\<close>.
+
+  \<^descr>[@{setting_def ISABELLE_PLATFORM_FAMILY}\<open>\<^sup>*\<close>] is automatically set to the
+  general platform family: \<^verbatim>\<open>linux\<close>, \<^verbatim>\<open>macos\<close>, \<^verbatim>\<open>windows\<close>. Note that
   platform-dependent tools usually need to refer to the more specific
   identification according to @{setting ISABELLE_PLATFORM}, @{setting
   ISABELLE_PLATFORM32}, @{setting ISABELLE_PLATFORM64}.
 
-  \<^descr>[@{setting_def ISABELLE_PLATFORM}\<open>\<^sup>*\<close>] is automatically
-  set to a symbolic identifier for the underlying hardware and
-  operating system.  The Isabelle platform identification always
-  refers to the 32 bit variant, even this is a 64 bit machine.  Note
-  that the ML or Java runtime may have a different idea, depending on
-  which binaries are actually run.
+  \<^descr>[@{setting_def ISABELLE_PLATFORM}\<open>\<^sup>*\<close>] is automatically set to a symbolic
+  identifier for the underlying hardware and operating system. The Isabelle
+  platform identification always refers to the 32 bit variant, even this is a
+  64 bit machine. Note that the ML or Java runtime may have a different idea,
+  depending on which binaries are actually run.
 
-  \<^descr>[@{setting_def ISABELLE_PLATFORM64}\<open>\<^sup>*\<close>] is similar to
-  @{setting ISABELLE_PLATFORM} but refers to the proper 64 bit variant
-  on a platform that supports this; the value is empty for 32 bit.
-  Note that the following bash expression (including the quotes)
-  prefers the 64 bit platform, if that is available:
+  \<^descr>[@{setting_def ISABELLE_PLATFORM64}\<open>\<^sup>*\<close>] is similar to @{setting
+  ISABELLE_PLATFORM} but refers to the proper 64 bit variant on a platform
+  that supports this; the value is empty for 32 bit. Note that the following
+  bash expression (including the quotes) prefers the 64 bit platform, if that
+  is available:
 
   @{verbatim [display] \<open>"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"\<close>}
 
-  \<^descr>[@{setting_def ISABELLE_PROCESS}\<open>\<^sup>*\<close>, @{setting
-  ISABELLE_TOOL}\<open>\<^sup>*\<close>] are automatically set to the full path
-  names of the @{executable "isabelle_process"} and @{executable
-  isabelle} executables, respectively.  Thus other tools and scripts
-  need not assume that the @{file "$ISABELLE_HOME/bin"} directory is
-  on the current search path of the shell.
-  
-  \<^descr>[@{setting_def ISABELLE_IDENTIFIER}\<open>\<^sup>*\<close>] refers
-  to the name of this Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2012\<close>''.
+  \<^descr>[@{setting_def ISABELLE_PROCESS}\<open>\<^sup>*\<close>, @{setting ISABELLE_TOOL}\<open>\<^sup>*\<close>] are
+  automatically set to the full path names of the @{executable
+  "isabelle_process"} and @{executable isabelle} executables, respectively.
+  Thus other tools and scripts need not assume that the @{file
+  "$ISABELLE_HOME/bin"} directory is on the current search path of the shell.
 
-  \<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME},
-  @{setting_def ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def
-  ML_IDENTIFIER}\<open>\<^sup>*\<close>] specify the underlying ML system
-  to be used for Isabelle.  There is only a fixed set of admissable
-  @{setting ML_SYSTEM} names (see the @{file
+  \<^descr>[@{setting_def ISABELLE_IDENTIFIER}\<open>\<^sup>*\<close>] refers to the name of this
+  Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2012\<close>''.
+
+  \<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, @{setting_def
+  ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def ML_IDENTIFIER}\<open>\<^sup>*\<close>]
+  specify the underlying ML system to be used for Isabelle. There is only a
+  fixed set of admissable @{setting ML_SYSTEM} names (see the @{file
   "$ISABELLE_HOME/etc/settings"} file of the distribution).
-  
+
   The actual compiler binary will be run from the directory @{setting
-  ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the
-  command line.  The optional @{setting ML_PLATFORM} may specify the
-  binary format of ML heap images, which is useful for cross-platform
-  installations.  The value of @{setting ML_IDENTIFIER} is
-  automatically obtained by composing the values of @{setting
-  ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version values.
+  ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the command line.
+  The optional @{setting ML_PLATFORM} may specify the binary format of ML heap
+  images, which is useful for cross-platform installations. The value of
+  @{setting ML_IDENTIFIER} is automatically obtained by composing the values
+  of @{setting ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version
+  values.
 
-  \<^descr>[@{setting_def ML_SYSTEM_POLYML}\<open>\<^sup>*\<close>] is \<^verbatim>\<open>true\<close>
-  for @{setting ML_SYSTEM} values derived from Poly/ML, as opposed to
-  SML/NJ where it is empty.  This is particularly useful with the
-  build option @{system_option condition}
-  (\secref{sec:system-options}) to restrict big sessions to something
-  that SML/NJ can still handle.
+  \<^descr>[@{setting_def ML_SYSTEM_POLYML}\<open>\<^sup>*\<close>] is \<^verbatim>\<open>true\<close> for @{setting ML_SYSTEM}
+  values derived from Poly/ML, as opposed to SML/NJ where it is empty. This is
+  particularly useful with the build option @{system_option condition}
+  (\secref{sec:system-options}) to restrict big sessions to something that
+  SML/NJ can still handle.
 
-  \<^descr>[@{setting_def ISABELLE_JDK_HOME}] needs to point to a full JDK
-  (Java Development Kit) installation with \<^verbatim>\<open>javac\<close> and
-  \<^verbatim>\<open>jar\<close> executables.  This is essential for Isabelle/Scala
-  and other JVM-based tools to work properly.  Note that conventional
-  \<^verbatim>\<open>JAVA_HOME\<close> usually points to the JRE (Java Runtime
+  \<^descr>[@{setting_def ISABELLE_JDK_HOME}] needs to point to a full JDK (Java
+  Development Kit) installation with \<^verbatim>\<open>javac\<close> and \<^verbatim>\<open>jar\<close> executables. This is
+  essential for Isabelle/Scala and other JVM-based tools to work properly.
+  Note that conventional \<^verbatim>\<open>JAVA_HOME\<close> usually points to the JRE (Java Runtime
   Environment), not JDK.
-  
-  \<^descr>[@{setting_def ISABELLE_PATH}] is a list of directories
-  (separated by colons) where Isabelle logic images may reside.  When
-  looking up heaps files, the value of @{setting ML_IDENTIFIER} is
-  appended to each component internally.
-  
-  \<^descr>[@{setting_def ISABELLE_OUTPUT}\<open>\<^sup>*\<close>] is a
-  directory where output heap files should be stored by default. The
-  ML system and Isabelle version identifier is appended here, too.
-  
-  \<^descr>[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where
-  theory browser information (HTML text, graph data, and printable
-  documents) is stored (see also \secref{sec:info}).  The default
-  value is @{file_unchecked "$ISABELLE_HOME_USER/browser_info"}.
-  
-  \<^descr>[@{setting_def ISABELLE_LOGIC}] specifies the default logic to
-  load if none is given explicitely by the user.  The default value is
-  \<^verbatim>\<open>HOL\<close>.
-  
-  \<^descr>[@{setting_def ISABELLE_LINE_EDITOR}] specifies the
-  line editor for the @{tool_ref console} interface.
+
+  \<^descr>[@{setting_def ISABELLE_PATH}] is a list of directories (separated by
+  colons) where Isabelle logic images may reside. When looking up heaps files,
+  the value of @{setting ML_IDENTIFIER} is appended to each component
+  internally.
+
+  \<^descr>[@{setting_def ISABELLE_OUTPUT}\<open>\<^sup>*\<close>] is a directory where output heap files
+  should be stored by default. The ML system and Isabelle version identifier
+  is appended here, too.
+
+  \<^descr>[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where theory
+  browser information (HTML text, graph data, and printable documents) is
+  stored (see also \secref{sec:info}). The default value is @{file_unchecked
+  "$ISABELLE_HOME_USER/browser_info"}.
+
+  \<^descr>[@{setting_def ISABELLE_LOGIC}] specifies the default logic to load if none
+  is given explicitely by the user. The default value is \<^verbatim>\<open>HOL\<close>.
+
+  \<^descr>[@{setting_def ISABELLE_LINE_EDITOR}] specifies the line editor for the
+  @{tool_ref console} interface.
 
-  \<^descr>[@{setting_def ISABELLE_LATEX}, @{setting_def
-  ISABELLE_PDFLATEX}, @{setting_def ISABELLE_BIBTEX}] refer to {\LaTeX}
-  related tools for Isabelle document preparation (see also
-  \secref{sec:tool-latex}).
-  
-  \<^descr>[@{setting_def ISABELLE_TOOLS}] is a colon separated list of
-  directories that are scanned by @{executable isabelle} for external
-  utility programs (see also \secref{sec:isabelle-tool}).
-  
-  \<^descr>[@{setting_def ISABELLE_DOCS}] is a colon separated list of
-  directories with documentation files.
+  \<^descr>[@{setting_def ISABELLE_LATEX}, @{setting_def ISABELLE_PDFLATEX},
+  @{setting_def ISABELLE_BIBTEX}] refer to {\LaTeX} related tools for Isabelle
+  document preparation (see also \secref{sec:tool-latex}).
+
+  \<^descr>[@{setting_def ISABELLE_TOOLS}] is a colon separated list of directories
+  that are scanned by @{executable isabelle} for external utility programs
+  (see also \secref{sec:isabelle-tool}).
 
-  \<^descr>[@{setting_def PDF_VIEWER}] specifies the program to be used
-  for displaying \<^verbatim>\<open>pdf\<close> files.
+  \<^descr>[@{setting_def ISABELLE_DOCS}] is a colon separated list of directories
+  with documentation files.
+
+  \<^descr>[@{setting_def PDF_VIEWER}] specifies the program to be used for displaying
+  \<^verbatim>\<open>pdf\<close> files.
 
-  \<^descr>[@{setting_def DVI_VIEWER}] specifies the program to be used
-  for displaying \<^verbatim>\<open>dvi\<close> files.
-  
-  \<^descr>[@{setting_def ISABELLE_TMP_PREFIX}\<open>\<^sup>*\<close>] is the
-  prefix from which any running @{executable "isabelle_process"}
-  derives an individual directory for temporary files.
+  \<^descr>[@{setting_def DVI_VIEWER}] specifies the program to be used for displaying
+  \<^verbatim>\<open>dvi\<close> files.
+
+  \<^descr>[@{setting_def ISABELLE_TMP_PREFIX}\<open>\<^sup>*\<close>] is the prefix from which any
+  running @{executable "isabelle_process"} derives an individual directory for
+  temporary files.
 \<close>
 
 
 subsection \<open>Additional components \label{sec:components}\<close>
 
-text \<open>Any directory may be registered as an explicit \<^emph>\<open>Isabelle
-  component\<close>.  The general layout conventions are that of the main
-  Isabelle distribution itself, and the following two files (both
-  optional) have a special meaning:
+text \<open>
+  Any directory may be registered as an explicit \<^emph>\<open>Isabelle component\<close>. The
+  general layout conventions are that of the main Isabelle distribution
+  itself, and the following two files (both optional) have a special meaning:
 
-  \<^item> \<^verbatim>\<open>etc/settings\<close> holds additional settings that are
-  initialized when bootstrapping the overall Isabelle environment,
-  cf.\ \secref{sec:boot}.  As usual, the content is interpreted as a
-  \<^verbatim>\<open>bash\<close> script.  It may refer to the component's enclosing
-  directory via the \<^verbatim>\<open>COMPONENT\<close> shell variable.
+    \<^item> \<^verbatim>\<open>etc/settings\<close> holds additional settings that are initialized when
+    bootstrapping the overall Isabelle environment, cf.\ \secref{sec:boot}. As
+    usual, the content is interpreted as a \<^verbatim>\<open>bash\<close> script. It may refer to the
+    component's enclosing directory via the \<^verbatim>\<open>COMPONENT\<close> shell variable.
 
-  For example, the following setting allows to refer to files within
-  the component later on, without having to hardwire absolute paths:
-  @{verbatim [display] \<open>MY_COMPONENT_HOME="$COMPONENT"\<close>}
+    For example, the following setting allows to refer to files within the
+    component later on, without having to hardwire absolute paths:
+    @{verbatim [display] \<open>MY_COMPONENT_HOME="$COMPONENT"\<close>}
 
-  Components can also add to existing Isabelle settings such as
-  @{setting_def ISABELLE_TOOLS}, in order to provide
-  component-specific tools that can be invoked by end-users.  For
-  example:
-  @{verbatim [display] \<open>ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"\<close>}
+    Components can also add to existing Isabelle settings such as
+    @{setting_def ISABELLE_TOOLS}, in order to provide component-specific
+    tools that can be invoked by end-users. For example:
+    @{verbatim [display] \<open>ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"\<close>}
 
-  \<^item> \<^verbatim>\<open>etc/components\<close> holds a list of further
-  sub-components of the same structure.  The directory specifications
-  given here can be either absolute (with leading \<^verbatim>\<open>/\<close>) or
-  relative to the component's main directory.
+    \<^item> \<^verbatim>\<open>etc/components\<close> holds a list of further sub-components of the same
+    structure. The directory specifications given here can be either absolute
+    (with leading \<^verbatim>\<open>/\<close>) or relative to the component's main directory.
 
-
-  The root of component initialization is @{setting ISABELLE_HOME}
-  itself.  After initializing all of its sub-components recursively,
-  @{setting ISABELLE_HOME_USER} is included in the same manner (if
-  that directory exists).  This allows to install private components
-  via @{file_unchecked "$ISABELLE_HOME_USER/etc/components"}, although it is
-  often more convenient to do that programmatically via the
-  \<^verbatim>\<open>init_component\<close> shell function in the \<^verbatim>\<open>etc/settings\<close>
-  script of \<^verbatim>\<open>$ISABELLE_HOME_USER\<close> (or any other component
-  directory).  For example:
+  The root of component initialization is @{setting ISABELLE_HOME} itself.
+  After initializing all of its sub-components recursively, @{setting
+  ISABELLE_HOME_USER} is included in the same manner (if that directory
+  exists). This allows to install private components via @{file_unchecked
+  "$ISABELLE_HOME_USER/etc/components"}, although it is often more convenient
+  to do that programmatically via the \<^verbatim>\<open>init_component\<close> shell function in the
+  \<^verbatim>\<open>etc/settings\<close> script of \<^verbatim>\<open>$ISABELLE_HOME_USER\<close> (or any other component
+  directory). For example:
   @{verbatim [display] \<open>init_component "$HOME/screwdriver-2.0"\<close>}
 
-  This is tolerant wrt.\ missing component directories, but might
-  produce a warning.
+  This is tolerant wrt.\ missing component directories, but might produce a
+  warning.
 
   \<^medskip>
-  More complex situations may be addressed by initializing
-  components listed in a given catalog file, relatively to some base
-  directory:
+  More complex situations may be addressed by initializing components listed
+  in a given catalog file, relatively to some base directory:
   @{verbatim [display] \<open>init_components "$HOME/my_component_store" "some_catalog_file"\<close>}
 
-  The component directories listed in the catalog file are treated as
-  relative to the given base directory.
+  The component directories listed in the catalog file are treated as relative
+  to the given base directory.
 
-  See also \secref{sec:tool-components} for some tool-support for
-  resolving components that are formally initialized but not installed
-  yet.
+  See also \secref{sec:tool-components} for some tool-support for resolving
+  components that are formally initialized but not installed yet.
 \<close>
 
 
 section \<open>The raw Isabelle process \label{sec:isabelle-process}\<close>
 
 text \<open>
-  The @{executable_def "isabelle_process"} executable runs bare-bones
-  Isabelle logic sessions --- either interactively or in batch mode.
-  It provides an abstraction over the underlying ML system, and over
-  the actual heap file locations.  Its usage is:
+  The @{executable_def "isabelle_process"} executable runs bare-bones Isabelle
+  logic sessions --- either interactively or in batch mode. It provides an
+  abstraction over the underlying ML system, and over the actual heap file
+  locations. Its usage is:
   @{verbatim [display]
 \<open>Usage: isabelle_process [OPTIONS] [INPUT] [OUTPUT]
 
@@ -349,123 +319,111 @@
   actual file names (containing at least one /).
   If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system.\<close>}
 
-  Input files without path specifications are looked up in the
-  @{setting ISABELLE_PATH} setting, which may consist of multiple
-  components separated by colons --- these are tried in the given
-  order with the value of @{setting ML_IDENTIFIER} appended
-  internally.  In a similar way, base names are relative to the
-  directory specified by @{setting ISABELLE_OUTPUT}.  In any case,
-  actual file locations may also be given by including at least one
-  slash (\<^verbatim>\<open>/\<close>) in the name (hint: use \<^verbatim>\<open>./\<close> to
-  refer to the current directory).
+  Input files without path specifications are looked up in the @{setting
+  ISABELLE_PATH} setting, which may consist of multiple components separated
+  by colons --- these are tried in the given order with the value of @{setting
+  ML_IDENTIFIER} appended internally. In a similar way, base names are
+  relative to the directory specified by @{setting ISABELLE_OUTPUT}. In any
+  case, actual file locations may also be given by including at least one
+  slash (\<^verbatim>\<open>/\<close>) in the name (hint: use \<^verbatim>\<open>./\<close> to refer to the current
+  directory).
 \<close>
 
 
 subsubsection \<open>Options\<close>
 
 text \<open>
-  If the input heap file does not have write permission bits set, or
-  the \<^verbatim>\<open>-r\<close> option is given explicitly, then the session
-  started will be read-only.  That is, the ML world cannot be
-  committed back into the image file.  Otherwise, a writable session
-  enables commits into either the input file, or into another output
-  heap file (if that is given as the second argument on the command
+  If the input heap file does not have write permission bits set, or the \<^verbatim>\<open>-r\<close>
+  option is given explicitly, then the session started will be read-only. That
+  is, the ML world cannot be committed back into the image file. Otherwise, a
+  writable session enables commits into either the input file, or into another
+  output heap file (if that is given as the second argument on the command
   line).
 
-  The read-write state of sessions is determined at startup only, it
-  cannot be changed intermediately. Also note that heap images may
-  require considerable amounts of disk space (hundreds of MB or some GB).
-  Users are responsible for themselves to dispose their heap files
-  when they are no longer needed.
+  The read-write state of sessions is determined at startup only, it cannot be
+  changed intermediately. Also note that heap images may require considerable
+  amounts of disk space (hundreds of MB or some GB). Users are responsible for
+  themselves to dispose their heap files when they are no longer needed.
 
   \<^medskip>
-  The \<^verbatim>\<open>-w\<close> option makes the output heap file
-  read-only after terminating.  Thus subsequent invocations cause the
-  logic image to be read-only automatically.
+  The \<^verbatim>\<open>-w\<close> option makes the output heap file read-only after terminating.
+  Thus subsequent invocations cause the logic image to be read-only
+  automatically.
 
   \<^medskip>
-  Using the \<^verbatim>\<open>-e\<close> option, arbitrary ML code may be
-  passed to the Isabelle session from the command line. Multiple
-  \<^verbatim>\<open>-e\<close> options are evaluated in the given order. Strange things
-  may happen when erroneous ML code is provided. Also make sure that
-  the ML commands are terminated properly by semicolon.
+  Using the \<^verbatim>\<open>-e\<close> option, arbitrary ML code may be passed to the Isabelle
+  session from the command line. Multiple \<^verbatim>\<open>-e\<close> options are evaluated in the
+  given order. Strange things may happen when erroneous ML code is provided.
+  Also make sure that the ML commands are terminated properly by semicolon.
 
   \<^medskip>
-  The \<^verbatim>\<open>-m\<close> option adds identifiers of print modes
-  to be made active for this session. Typically, this is used by some
-  user interface, e.g.\ to enable output of proper mathematical
-  symbols.
+  The \<^verbatim>\<open>-m\<close> option adds identifiers of print modes to be made active for this
+  session. Typically, this is used by some user interface, e.g.\ to enable
+  output of proper mathematical symbols.
 
   \<^medskip>
-  Isabelle normally enters an interactive top-level loop
-  (after processing the \<^verbatim>\<open>-e\<close> texts). The \<^verbatim>\<open>-q\<close>
-  option inhibits interaction, thus providing a pure batch mode
-  facility.
+  Isabelle normally enters an interactive top-level loop (after processing the
+  \<^verbatim>\<open>-e\<close> texts). The \<^verbatim>\<open>-q\<close> option inhibits interaction, thus providing a pure
+  batch mode facility.
 
   \<^medskip>
-  Option \<^verbatim>\<open>-o\<close> allows to override Isabelle system
-  options for this process, see also \secref{sec:system-options}.
-  Alternatively, option \<^verbatim>\<open>-O\<close> specifies the full environment of
-  system options as a file in YXML format (according to the Isabelle/Scala
-  function \<^verbatim>\<open>isabelle.Options.encode\<close>).
+  Option \<^verbatim>\<open>-o\<close> allows to override Isabelle system options for this process,
+  see also \secref{sec:system-options}. Alternatively, option \<^verbatim>\<open>-O\<close> specifies
+  the full environment of system options as a file in YXML format (according
+  to the Isabelle/Scala function \<^verbatim>\<open>isabelle.Options.encode\<close>).
 
   \<^medskip>
-  The \<^verbatim>\<open>-P\<close> option starts the Isabelle process wrapper
-  for Isabelle/Scala, with a private protocol running over the specified TCP
-  socket. Isabelle/ML and Isabelle/Scala provide various programming
-  interfaces to invoke protocol functions over untyped strings and XML
-  trees.
+  The \<^verbatim>\<open>-P\<close> option starts the Isabelle process wrapper for Isabelle/Scala,
+  with a private protocol running over the specified TCP socket. Isabelle/ML
+  and Isabelle/Scala provide various programming interfaces to invoke protocol
+  functions over untyped strings and XML trees.
 
   \<^medskip>
-  The \<^verbatim>\<open>-S\<close> option makes the Isabelle process more
-  secure by disabling some critical operations, notably runtime
-  compilation and evaluation of ML source code.
+  The \<^verbatim>\<open>-S\<close> option makes the Isabelle process more secure by disabling some
+  critical operations, notably runtime compilation and evaluation of ML source
+  code.
 \<close>
 
 
 subsubsection \<open>Examples\<close>
 
 text \<open>
-  Run an interactive session of the default object-logic (as specified
-  by the @{setting ISABELLE_LOGIC} setting) like this:
+  Run an interactive session of the default object-logic (as specified by the
+  @{setting ISABELLE_LOGIC} setting) like this:
   @{verbatim [display] \<open>isabelle_process\<close>}
 
-  Usually @{setting ISABELLE_LOGIC} refers to one of the standard
-  logic images, which are read-only by default.  A writable session
-  --- based on \<^verbatim>\<open>HOL\<close>, but output to \<^verbatim>\<open>Test\<close> (in the
-  directory specified by the @{setting ISABELLE_OUTPUT} setting) ---
-  may be invoked as follows:
+  Usually @{setting ISABELLE_LOGIC} refers to one of the standard logic
+  images, which are read-only by default. A writable session --- based on
+  \<^verbatim>\<open>HOL\<close>, but output to \<^verbatim>\<open>Test\<close> (in the directory specified by the @{setting
+  ISABELLE_OUTPUT} setting) --- may be invoked as follows:
   @{verbatim [display] \<open>isabelle_process HOL Test\<close>}
 
-  Ending this session normally (e.g.\ by typing control-D) dumps the
-  whole ML system state into \<^verbatim>\<open>Test\<close> (be prepared for more
-  than 100\,MB):
+  Ending this session normally (e.g.\ by typing control-D) dumps the whole ML
+  system state into \<^verbatim>\<open>Test\<close> (be prepared for more than 100\,MB):
 
-  The \<^verbatim>\<open>Test\<close> session may be continued later (still in
-  writable state) by: @{verbatim [display] \<open>isabelle_process Test\<close>}
+  The \<^verbatim>\<open>Test\<close> session may be continued later (still in writable state) by:
+  @{verbatim [display] \<open>isabelle_process Test\<close>}
 
   A read-only \<^verbatim>\<open>Test\<close> session may be started by:
   @{verbatim [display] \<open>isabelle_process -r Test\<close>}
 
   \<^bigskip>
-  The next example demonstrates batch execution of Isabelle.
-  We retrieve the \<^verbatim>\<open>Main\<close> theory value from the theory loader
-  within ML (observe the delicate quoting rules for the Bash shell
-  vs.\ ML):
+  The next example demonstrates batch execution of Isabelle. We retrieve the
+  \<^verbatim>\<open>Main\<close> theory value from the theory loader within ML (observe the delicate
+  quoting rules for the Bash shell vs.\ ML):
   @{verbatim [display] \<open>isabelle_process -e 'Thy_Info.get_theory "Main";' -q -r HOL\<close>}
 
-  Note that the output text will be interspersed with additional junk
-  messages by the ML runtime environment.  The \<^verbatim>\<open>-W\<close> option
-  allows to communicate with the Isabelle process via an external
-  program in a more robust fashion.
+  Note that the output text will be interspersed with additional junk messages
+  by the ML runtime environment. The \<^verbatim>\<open>-W\<close> option allows to communicate with
+  the Isabelle process via an external program in a more robust fashion.
 \<close>
 
 
 section \<open>The Isabelle tool wrapper \label{sec:isabelle-tool}\<close>
 
 text \<open>
-  All Isabelle related tools and interfaces are called via a common
-  wrapper --- @{executable isabelle}:
+  All Isabelle related tools and interfaces are called via a common wrapper
+  --- @{executable isabelle}:
   @{verbatim [display]
 \<open>Usage: isabelle TOOL [ARGS ...]
 
@@ -474,20 +432,19 @@
 Available tools:
   ...\<close>}
 
-  In principle, Isabelle tools are ordinary executable scripts that
-  are run within the Isabelle settings environment, see
-  \secref{sec:settings}.  The set of available tools is collected by
-  @{executable isabelle} from the directories listed in the @{setting
-  ISABELLE_TOOLS} setting.  Do not try to call the scripts directly
-  from the shell.  Neither should you add the tool directories to your
-  shell's search path!
+  In principle, Isabelle tools are ordinary executable scripts that are run
+  within the Isabelle settings environment, see \secref{sec:settings}. The set
+  of available tools is collected by @{executable isabelle} from the
+  directories listed in the @{setting ISABELLE_TOOLS} setting. Do not try to
+  call the scripts directly from the shell. Neither should you add the tool
+  directories to your shell's search path!
 \<close>
 
 
 subsubsection \<open>Examples\<close>
 
-text \<open>Show the list of available documentation of the Isabelle
-  distribution:
+text \<open>
+  Show the list of available documentation of the Isabelle distribution:
   @{verbatim [display] \<open>isabelle doc\<close>}
 
   View a certain document as follows:
diff -r e717f152d2a8 -r f18f6e51e901 src/Doc/System/Misc.thy
--- a/src/Doc/System/Misc.thy	Wed Nov 04 19:52:38 2015 +0100
+++ b/src/Doc/System/Misc.thy	Wed Nov 04 20:18:46 2015 +0100
@@ -1,3 +1,5 @@
+(*:wrap=hard:maxLineLen=78:*)
+
 theory Misc
 imports Base
 begin
@@ -5,25 +7,27 @@
 chapter \<open>Miscellaneous tools \label{ch:tools}\<close>
 
 text \<open>
-  Subsequently we describe various Isabelle related utilities, given
-  in alphabetical order.
+  Subsequently we describe various Isabelle related utilities, given in
+  alphabetical order.
 \<close>
 
 
 section \<open>Theory graph browser \label{sec:browse}\<close>
 
-text \<open>The Isabelle graph browser is a general tool for visualizing
-  dependency graphs.  Certain nodes of the graph (i.e.\ theories) can
-  be grouped together in ``directories'', whose contents may be
-  hidden, thus enabling the user to collapse irrelevant portions of
-  information.  The browser is written in Java, it can be used both as
-  a stand-alone application and as an applet.\<close>
+text \<open>
+  The Isabelle graph browser is a general tool for visualizing dependency
+  graphs. Certain nodes of the graph (i.e.\ theories) can be grouped together
+  in ``directories'', whose contents may be hidden, thus enabling the user to
+  collapse irrelevant portions of information. The browser is written in Java,
+  it can be used both as a stand-alone application and as an applet.
+\<close>
 
 
 subsection \<open>Invoking the graph browser\<close>
 
-text \<open>The stand-alone version of the graph browser is wrapped up as
-  @{tool_def browser}:
+text \<open>
+  The stand-alone version of the graph browser is wrapped up as @{tool_def
+  browser}:
   @{verbatim [display]
 \<open>Usage: isabelle browser [OPTIONS] [GRAPHFILE]
 
@@ -32,35 +36,31 @@
     -c           cleanup -- remove GRAPHFILE after use
     -o FILE      output to FILE (ps, eps, pdf)\<close>}
 
-  When no file name is specified, the browser automatically changes to
-  the directory @{setting ISABELLE_BROWSER_INFO}.
+  When no file name is specified, the browser automatically changes to the
+  directory @{setting ISABELLE_BROWSER_INFO}.
 
   \<^medskip>
-  The \<^verbatim>\<open>-b\<close> option indicates that this is for
-  administrative build only, i.e.\ no browser popup if no files are
-  given.
+  The \<^verbatim>\<open>-b\<close> option indicates that this is for administrative build only, i.e.\
+  no browser popup if no files are given.
 
-  The \<^verbatim>\<open>-c\<close> option causes the input file to be removed
-  after use.
+  The \<^verbatim>\<open>-c\<close> option causes the input file to be removed after use.
 
-  The \<^verbatim>\<open>-o\<close> option indicates batch-mode operation, with the
-  output written to the indicated file; note that \<^verbatim>\<open>pdf\<close>
-  produces an \<^verbatim>\<open>eps\<close> copy as well.
+  The \<^verbatim>\<open>-o\<close> option indicates batch-mode operation, with the output written to
+  the indicated file; note that \<^verbatim>\<open>pdf\<close> produces an \<^verbatim>\<open>eps\<close> copy as well.
 
   \<^medskip>
-  The applet version of the browser is part of the standard
-  WWW theory presentation, see the link ``theory dependencies'' within
-  each session index.
+  The applet version of the browser is part of the standard WWW theory
+  presentation, see the link ``theory dependencies'' within each session
+  index.
 \<close>
 
 
 subsection \<open>Using the graph browser\<close>
 
 text \<open>
-  The browser's main window, which is shown in
-  \figref{fig:browserwindow}, consists of two sub-windows.  In the
-  left sub-window, the directory tree is displayed. The graph itself
-  is displayed in the right sub-window.
+  The browser's main window, which is shown in \figref{fig:browserwindow},
+  consists of two sub-windows. In the left sub-window, the directory tree is
+  displayed. The graph itself is displayed in the right sub-window.
 
   \begin{figure}[ht]
   \includegraphics[width=\textwidth]{browser_screenshot}
@@ -72,63 +72,57 @@
 subsubsection \<open>The directory tree window\<close>
 
 text \<open>
-  We describe the usage of the directory browser and the meaning of
-  the different items in the browser window.
+  We describe the usage of the directory browser and the meaning of the
+  different items in the browser window.
 
-  \<^item> A red arrow before a directory name indicates that the
-  directory is currently ``folded'', i.e.~the nodes in this directory
-  are collapsed to one single node. In the right sub-window, the names
-  of nodes corresponding to folded directories are enclosed in square
-  brackets and displayed in red color.
+  \<^item> A red arrow before a directory name indicates that the directory is
+  currently ``folded'', i.e.~the nodes in this directory are collapsed to one
+  single node. In the right sub-window, the names of nodes corresponding to
+  folded directories are enclosed in square brackets and displayed in red
+  color.
 
-  \<^item> A green downward arrow before a directory name indicates that
-  the directory is currently ``unfolded''. It can be folded by
-  clicking on the directory name.  Clicking on the name for a second
-  time unfolds the directory again.  Alternatively, a directory can
-  also be unfolded by clicking on the corresponding node in the right
-  sub-window.
+  \<^item> A green downward arrow before a directory name indicates that the
+  directory is currently ``unfolded''. It can be folded by clicking on the
+  directory name. Clicking on the name for a second time unfolds the directory
+  again. Alternatively, a directory can also be unfolded by clicking on the
+  corresponding node in the right sub-window.
 
-  \<^item> Blue arrows stand before ordinary node names. When clicking on
-  such a name (i.e.\ that of a theory), the graph display window
-  focuses to the corresponding node. Double clicking invokes a text
-  viewer window in which the contents of the theory file are
-  displayed.
+  \<^item> Blue arrows stand before ordinary node names. When clicking on such a name
+  (i.e.\ that of a theory), the graph display window focuses to the
+  corresponding node. Double clicking invokes a text viewer window in which
+  the contents of the theory file are displayed.
 \<close>
 
 
 subsubsection \<open>The graph display window\<close>
 
 text \<open>
-  When pointing on an ordinary node, an upward and a downward arrow is
-  shown.  Initially, both of these arrows are green. Clicking on the
-  upward or downward arrow collapses all predecessor or successor
-  nodes, respectively. The arrow's color then changes to red,
-  indicating that the predecessor or successor nodes are currently
-  collapsed. The node corresponding to the collapsed nodes has the
-  name ``\<^verbatim>\<open>[....]\<close>''. To uncollapse the nodes again, simply
-  click on the red arrow or on the node with the name ``\<^verbatim>\<open>[....]\<close>''.
-  Similar to the directory browser, the contents of
-  theory files can be displayed by double clicking on the
-  corresponding node.
+  When pointing on an ordinary node, an upward and a downward arrow is shown.
+  Initially, both of these arrows are green. Clicking on the upward or
+  downward arrow collapses all predecessor or successor nodes, respectively.
+  The arrow's color then changes to red, indicating that the predecessor or
+  successor nodes are currently collapsed. The node corresponding to the
+  collapsed nodes has the name ``\<^verbatim>\<open>[....]\<close>''. To uncollapse the nodes again,
+  simply click on the red arrow or on the node with the name ``\<^verbatim>\<open>[....]\<close>''.
+  Similar to the directory browser, the contents of theory files can be
+  displayed by double clicking on the corresponding node.
 \<close>
 
 
 subsubsection \<open>The ``File'' menu\<close>
 
 text \<open>
-  Due to Java Applet security restrictions this menu is only available
-  in the full application version. The meaning of the menu items is as
-  follows:
+  Due to Java Applet security restrictions this menu is only available in the
+  full application version. The meaning of the menu items is as follows:
 
   \<^descr>[Open \dots] Open a new graph file.
 
-  \<^descr>[Export to PostScript] Outputs the current graph in Postscript
-  format, appropriately scaled to fit on one single sheet of A4 paper.
-  The resulting file can be printed directly.
+  \<^descr>[Export to PostScript] Outputs the current graph in Postscript format,
+  appropriately scaled to fit on one single sheet of A4 paper. The resulting
+  file can be printed directly.
 
-  \<^descr>[Export to EPS] Outputs the current graph in Encapsulated
-  Postscript format. The resulting file can be included in other
-  documents.
+  \<^descr>[Export to EPS] Outputs the current graph in Encapsulated Postscript
+  format. The resulting file can be included in other documents.
 
   \<^descr>[Quit] Quit the graph browser.
 \<close>
@@ -150,22 +144,20 @@
 
   \<^descr>[\<open>vertex_name\<close>] The name of the vertex.
 
-  \<^descr>[\<open>vertex_ID\<close>] The vertex identifier. Note that there may
-  be several vertices with equal names, whereas identifiers must be
-  unique.
+  \<^descr>[\<open>vertex_ID\<close>] The vertex identifier. Note that there may be several
+  vertices with equal names, whereas identifiers must be unique.
 
-  \<^descr>[\<open>dir_name\<close>] The name of the ``directory'' the vertex
-  should be placed in.  A ``\<^verbatim>\<open>+\<close>'' sign after \<open>dir_name\<close> indicates that the nodes in the directory are initially
-  visible. Directories are initially invisible by default.
+  \<^descr>[\<open>dir_name\<close>] The name of the ``directory'' the vertex should be placed in.
+  A ``\<^verbatim>\<open>+\<close>'' sign after \<open>dir_name\<close> indicates that the nodes in the directory
+  are initially visible. Directories are initially invisible by default.
 
-  \<^descr>[\<open>path\<close>] The path of the corresponding theory file. This
-  is specified relatively to the path of the graph definition file.
+  \<^descr>[\<open>path\<close>] The path of the corresponding theory file. This is specified
+  relatively to the path of the graph definition file.
 
-  \<^descr>[List of successor/predecessor nodes] A ``\<^verbatim>\<open><\<close>''
-  sign before the list means that successor nodes are listed, a
-  ``\<^verbatim>\<open>>\<close>'' sign means that predecessor nodes are listed. If
-  neither ``\<^verbatim>\<open><\<close>'' nor ``\<^verbatim>\<open>>\<close>'' is found, the
-  browser assumes that successor nodes are listed.
+  \<^descr>[List of successor/predecessor nodes] A ``\<^verbatim>\<open><\<close>'' sign before the list means
+  that successor nodes are listed, a ``\<^verbatim>\<open>>\<close>'' sign means that predecessor
+  nodes are listed. If neither ``\<^verbatim>\<open><\<close>'' nor ``\<^verbatim>\<open>>\<close>'' is found, the browser
+  assumes that successor nodes are listed.
 \<close>
 
 
@@ -188,33 +180,28 @@
 
   ISABELLE_COMPONENT_REPOSITORY="http://isabelle.in.tum.de/components"\<close>}
 
-  Components are initialized as described in \secref{sec:components}
-  in a permissive manner, which can mark components as ``missing''.
-  This state is amended by letting @{tool "components"} download and
-  unpack components that are published on the default component
-  repository @{url "http://isabelle.in.tum.de/components/"} in
-  particular.
+  Components are initialized as described in \secref{sec:components} in a
+  permissive manner, which can mark components as ``missing''. This state is
+  amended by letting @{tool "components"} download and unpack components that
+  are published on the default component repository @{url
+  "http://isabelle.in.tum.de/components/"} in particular.
 
-  Option \<^verbatim>\<open>-R\<close> specifies an alternative component
-  repository.  Note that \<^verbatim>\<open>file:///\<close> URLs can be used for
-  local directories.
+  Option \<^verbatim>\<open>-R\<close> specifies an alternative component repository. Note that
+  \<^verbatim>\<open>file:///\<close> URLs can be used for local directories.
 
-  Option \<^verbatim>\<open>-a\<close> selects all missing components to be
-  resolved.  Explicit components may be named as command
-  line-arguments as well.  Note that components are uniquely
-  identified by their base name, while the installation takes place in
-  the location that was specified in the attempt to initialize the
-  component before.
+  Option \<^verbatim>\<open>-a\<close> selects all missing components to be resolved. Explicit
+  components may be named as command line-arguments as well. Note that
+  components are uniquely identified by their base name, while the
+  installation takes place in the location that was specified in the attempt
+  to initialize the component before.
 
-  Option \<^verbatim>\<open>-l\<close> lists the current state of available and
-  missing components with their location (full name) within the
-  file-system.
+  Option \<^verbatim>\<open>-l\<close> lists the current state of available and missing components
+  with their location (full name) within the file-system.
 
-  Option \<^verbatim>\<open>-I\<close> initializes the user settings file to
-  subscribe to the standard components specified in the Isabelle
-  repository clone --- this does not make any sense for regular
-  Isabelle releases.  If the file already exists, it needs to be
-  edited manually according to the printed explanation.
+  Option \<^verbatim>\<open>-I\<close> initializes the user settings file to subscribe to the standard
+  components specified in the Isabelle repository clone --- this does not make
+  any sense for regular Isabelle releases. If the file already exists, it
+  needs to be edited manually according to the printed explanation.
 \<close>
 
 
@@ -236,14 +223,14 @@
   Run Isabelle process with raw ML console and line editor
   (default ISABELLE_LINE_EDITOR).\<close>}
 
-  The \<^verbatim>\<open>-l\<close> option specifies the logic session name. By default,
-  its heap image is checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that.
+  The \<^verbatim>\<open>-l\<close> option specifies the logic session name. By default, its heap
+  image is checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that.
 
-  Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-o\<close>, \<^verbatim>\<open>-s\<close> are passed
-  directly to @{tool build} (\secref{sec:tool-build}).
+  Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-o\<close>, \<^verbatim>\<open>-s\<close> are passed directly to @{tool build}
+  (\secref{sec:tool-build}).
 
-  Options \<^verbatim>\<open>-m\<close>, \<^verbatim>\<open>-o\<close> are passed directly to the
-  underlying Isabelle process (\secref{sec:isabelle-process}).
+  Options \<^verbatim>\<open>-m\<close>, \<^verbatim>\<open>-o\<close> are passed directly to the underlying Isabelle process
+  (\secref{sec:isabelle-process}).
 
   The Isabelle process is run through the line editor that is specified via
   the settings variable @{setting ISABELLE_LINE_EDITOR} (e.g.\
@@ -259,19 +246,18 @@
 
 section \<open>Displaying documents \label{sec:tool-display}\<close>
 
-text \<open>The @{tool_def display} tool displays documents in DVI or PDF
-  format:
+text \<open>
+  The @{tool_def display} tool displays documents in DVI or PDF format:
   @{verbatim [display]
 \<open>Usage: isabelle display DOCUMENT
 
   Display DOCUMENT (in DVI or PDF format).\<close>}
 
   \<^medskip>
-  The settings @{setting DVI_VIEWER} and @{setting
-  PDF_VIEWER} determine the programs for viewing the corresponding
-  file formats.  Normally this opens the document via the desktop
-  environment, potentially in an asynchronous manner with re-use of
-  previews views.
+  The settings @{setting DVI_VIEWER} and @{setting PDF_VIEWER} determine the
+  programs for viewing the corresponding file formats. Normally this opens the
+  document via the desktop environment, potentially in an asynchronous manner
+  with re-use of previews views.
 \<close>
 
 
@@ -284,27 +270,27 @@
 
   View Isabelle documentation.\<close>}
 
-  If called without arguments, it lists all available documents. Each
-  line starts with an identifier, followed by a short description. Any
-  of these identifiers may be specified as arguments, in order to
-  display the corresponding document (see also
-  \secref{sec:tool-display}).
+  If called without arguments, it lists all available documents. Each line
+  starts with an identifier, followed by a short description. Any of these
+  identifiers may be specified as arguments, in order to display the
+  corresponding document (see also \secref{sec:tool-display}).
 
   \<^medskip>
-  The @{setting ISABELLE_DOCS} setting specifies the list of
-  directories (separated by colons) to be scanned for documentations.
+  The @{setting ISABELLE_DOCS} setting specifies the list of directories
+  (separated by colons) to be scanned for documentations.
 \<close>
 
 
 section \<open>Shell commands within the settings environment \label{sec:tool-env}\<close>
 
-text \<open>The @{tool_def env} tool is a direct wrapper for the standard
-  \<^verbatim>\<open>/usr/bin/env\<close> command on POSIX systems, running within
-  the Isabelle settings environment (\secref{sec:settings}).
+text \<open>
+  The @{tool_def env} tool is a direct wrapper for the standard
+  \<^verbatim>\<open>/usr/bin/env\<close> command on POSIX systems, running within the Isabelle
+  settings environment (\secref{sec:settings}).
 
-  The command-line arguments are that of the underlying version of
-  \<^verbatim>\<open>env\<close>.  For example, the following invokes an instance of
-  the GNU Bash shell within the Isabelle environment:
+  The command-line arguments are that of the underlying version of \<^verbatim>\<open>env\<close>. For
+  example, the following invokes an instance of the GNU Bash shell within the
+  Isabelle environment:
   @{verbatim [display] \<open>isabelle env bash\<close>}
 \<close>
 
@@ -325,38 +311,39 @@
 
   Get value of VARNAMES from the Isabelle settings.\<close>}
 
-  With the \<^verbatim>\<open>-a\<close> option, one may inspect the full process
-  environment that Isabelle related programs are run in. This usually
-  contains much more variables than are actually Isabelle settings.
-  Normally, output is a list of lines of the form \<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close>. The \<^verbatim>\<open>-b\<close> option
-  causes only the values to be printed.
+  With the \<^verbatim>\<open>-a\<close> option, one may inspect the full process environment that
+  Isabelle related programs are run in. This usually contains much more
+  variables than are actually Isabelle settings. Normally, output is a list of
+  lines of the form \<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close>. The \<^verbatim>\<open>-b\<close> option causes only the values
+  to be printed.
 
-  Option \<^verbatim>\<open>-d\<close> produces a dump of the complete environment
-  to the specified file.  Entries are terminated by the ASCII null
-  character, i.e.\ the C string terminator.
+  Option \<^verbatim>\<open>-d\<close> produces a dump of the complete environment to the specified
+  file. Entries are terminated by the ASCII null character, i.e.\ the C string
+  terminator.
 \<close>
 
 
 subsubsection \<open>Examples\<close>
 
-text \<open>Get the location of @{setting ISABELLE_HOME_USER} where
-  user-specific information is stored:
+text \<open>
+  Get the location of @{setting ISABELLE_HOME_USER} where user-specific
+  information is stored:
   @{verbatim [display] \<open>isabelle getenv ISABELLE_HOME_USER\<close>}
 
   \<^medskip>
-  Get the value only of the same settings variable, which is
-  particularly useful in shell scripts:
+  Get the value only of the same settings variable, which is particularly
+  useful in shell scripts:
   @{verbatim [display] \<open>isabelle getenv -b ISABELLE_OUTPUT\<close>}
 \<close>
 
 
 section \<open>Installing standalone Isabelle executables \label{sec:tool-install}\<close>
 
-text \<open>By default, the main Isabelle binaries (@{executable
-  "isabelle"} etc.)  are just run from their location within the
-  distribution directory, probably indirectly by the shell through its
-  @{setting PATH}.  Other schemes of installation are supported by the
-  @{tool_def install} tool:
+text \<open>
+  By default, the main Isabelle binaries (@{executable "isabelle"} etc.) are
+  just run from their location within the distribution directory, probably
+  indirectly by the shell through its @{setting PATH}. Other schemes of
+  installation are supported by the @{tool_def install} tool:
   @{verbatim [display]
 \<open>Usage: isabelle install [OPTIONS] BINDIR
 
@@ -367,24 +354,26 @@
   Install Isabelle executables with absolute references to the
   distribution directory.\<close>}
 
-  The \<^verbatim>\<open>-d\<close> option overrides the current Isabelle
-  distribution directory as determined by @{setting ISABELLE_HOME}.
+  The \<^verbatim>\<open>-d\<close> option overrides the current Isabelle distribution directory as
+  determined by @{setting ISABELLE_HOME}.
 
-  The \<open>BINDIR\<close> argument tells where executable wrapper scripts
-  for @{executable "isabelle_process"} and @{executable isabelle}
-  should be placed, which is typically a directory in the shell's
-  @{setting PATH}, such as \<^verbatim>\<open>$HOME/bin\<close>.
+  The \<open>BINDIR\<close> argument tells where executable wrapper scripts for
+  @{executable "isabelle_process"} and @{executable isabelle} should be
+  placed, which is typically a directory in the shell's @{setting PATH}, such
+  as \<^verbatim>\<open>$HOME/bin\<close>.
 
   \<^medskip>
-  It is also possible to make symbolic links of the main
-  Isabelle executables manually, but making separate copies outside
-  the Isabelle distribution directory will not work!\<close>
+  It is also possible to make symbolic links of the main Isabelle executables
+  manually, but making separate copies outside the Isabelle distribution
+  directory will not work!
+\<close>
 
 
 section \<open>Creating instances of the Isabelle logo\<close>
 
-text \<open>The @{tool_def logo} tool creates instances of the generic
-  Isabelle logo as EPS and PDF, for inclusion in {\LaTeX} documents.
+text \<open>
+  The @{tool_def logo} tool creates instances of the generic Isabelle logo as
+  EPS and PDF, for inclusion in {\LaTeX} documents.
   @{verbatim [display]
 \<open>Usage: isabelle logo [OPTIONS] XYZ
 
@@ -394,16 +383,15 @@
     -n NAME      alternative output base name (default "isabelle_xyx")
     -q           quiet mode\<close>}
 
-  Option \<^verbatim>\<open>-n\<close> specifies an alternative (base) name for the
-  generated files.  The default is \<^verbatim>\<open>isabelle_\<close>\<open>xyz\<close>
-  in lower-case.
+  Option \<^verbatim>\<open>-n\<close> specifies an alternative (base) name for the generated files.
+  The default is \<^verbatim>\<open>isabelle_\<close>\<open>xyz\<close> in lower-case.
 
   Option \<^verbatim>\<open>-q\<close> omits printing of the result file name.
 
   \<^medskip>
-  Implementors of Isabelle tools and applications are
-  encouraged to make derived Isabelle logos for their own projects
-  using this template.\<close>
+  Implementors of Isabelle tools and applications are encouraged to make
+  derived Isabelle logos for their own projects using this template.
+\<close>
 
 
 section \<open>Output the version identifier of the Isabelle distribution\<close>
@@ -419,53 +407,49 @@
   Display Isabelle version information.\<close>}
 
   \<^medskip>
-  The default is to output the full version string of the
-  Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2012: May 2012\<close>.
+  The default is to output the full version string of the Isabelle
+  distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2012: May 2012\<close>.
 
-  The \<^verbatim>\<open>-i\<close> option produces a short identification derived
-  from the Mercurial id of the @{setting ISABELLE_HOME} directory.
+  The \<^verbatim>\<open>-i\<close> option produces a short identification derived from the Mercurial
+  id of the @{setting ISABELLE_HOME} directory.
 \<close>
 
 
 section \<open>Convert XML to YXML\<close>
 
 text \<open>
-  The @{tool_def yxml} tool converts a standard XML document (stdin)
-  to the much simpler and more efficient YXML format of Isabelle
-  (stdout).  The YXML format is defined as follows.
-
-  \<^enum> The encoding is always UTF-8.
+  The @{tool_def yxml} tool converts a standard XML document (stdin) to the
+  much simpler and more efficient YXML format of Isabelle (stdout). The YXML
+  format is defined as follows.
 
-  \<^enum> Body text is represented verbatim (no escaping, no special
-  treatment of white space, no named entities, no CDATA chunks, no
-  comments).
+    \<^enum> The encoding is always UTF-8.
 
-  \<^enum> Markup elements are represented via ASCII control characters
-  \<open>\<^bold>X = 5\<close> and \<open>\<^bold>Y = 6\<close> as follows:
+    \<^enum> Body text is represented verbatim (no escaping, no special treatment of
+    white space, no named entities, no CDATA chunks, no comments).
 
-  \begin{tabular}{ll}
-    XML & YXML \\\hline
-    \<^verbatim>\<open><\<close>\<open>name attribute\<close>\<^verbatim>\<open>=\<close>\<open>value \<dots>\<close>\<^verbatim>\<open>>\<close> &
-    \<open>\<^bold>X\<^bold>Yname\<^bold>Yattribute\<close>\<^verbatim>\<open>=\<close>\<open>value\<dots>\<^bold>X\<close> \\
-    \<^verbatim>\<open></\<close>\<open>name\<close>\<^verbatim>\<open>>\<close> & \<open>\<^bold>X\<^bold>Y\<^bold>X\<close> \\
-  \end{tabular}
+    \<^enum> Markup elements are represented via ASCII control characters \<open>\<^bold>X = 5\<close>
+    and \<open>\<^bold>Y = 6\<close> as follows:
 
-  There is no special case for empty body text, i.e.\ \<^verbatim>\<open><foo/>\<close>
-  is treated like \<^verbatim>\<open><foo></foo>\<close>.  Also note that
-  \<open>\<^bold>X\<close> and \<open>\<^bold>Y\<close> may never occur in
-  well-formed XML documents.
+    \begin{tabular}{ll}
+      XML & YXML \\\hline
+      \<^verbatim>\<open><\<close>\<open>name attribute\<close>\<^verbatim>\<open>=\<close>\<open>value \<dots>\<close>\<^verbatim>\<open>>\<close> &
+      \<open>\<^bold>X\<^bold>Yname\<^bold>Yattribute\<close>\<^verbatim>\<open>=\<close>\<open>value\<dots>\<^bold>X\<close> \\
+      \<^verbatim>\<open></\<close>\<open>name\<close>\<^verbatim>\<open>>\<close> & \<open>\<^bold>X\<^bold>Y\<^bold>X\<close> \\
+    \end{tabular}
 
+    There is no special case for empty body text, i.e.\ \<^verbatim>\<open><foo/>\<close> is treated
+    like \<^verbatim>\<open><foo></foo>\<close>. Also note that \<open>\<^bold>X\<close> and \<open>\<^bold>Y\<close> may never occur in
+    well-formed XML documents.
 
   Parsing YXML is pretty straight-forward: split the text into chunks
-  separated by \<open>\<^bold>X\<close>, then split each chunk into
-  sub-chunks separated by \<open>\<^bold>Y\<close>.  Markup chunks start
-  with an empty sub-chunk, and a second empty sub-chunk indicates
-  close of an element.  Any other non-empty chunk consists of plain
-  text.  For example, see @{file "~~/src/Pure/PIDE/yxml.ML"} or
-  @{file "~~/src/Pure/PIDE/yxml.scala"}.
+  separated by \<open>\<^bold>X\<close>, then split each chunk into sub-chunks separated by \<open>\<^bold>Y\<close>.
+  Markup chunks start with an empty sub-chunk, and a second empty sub-chunk
+  indicates close of an element. Any other non-empty chunk consists of plain
+  text. For example, see @{file "~~/src/Pure/PIDE/yxml.ML"} or @{file
+  "~~/src/Pure/PIDE/yxml.scala"}.
 
-  YXML documents may be detected quickly by checking that the first
-  two characters are \<open>\<^bold>X\<^bold>Y\<close>.
+  YXML documents may be detected quickly by checking that the first two
+  characters are \<open>\<^bold>X\<^bold>Y\<close>.
 \<close>
 
 end
\ No newline at end of file
diff -r e717f152d2a8 -r f18f6e51e901 src/Doc/System/Presentation.thy
--- a/src/Doc/System/Presentation.thy	Wed Nov 04 19:52:38 2015 +0100
+++ b/src/Doc/System/Presentation.thy	Wed Nov 04 20:18:46 2015 +0100
@@ -1,24 +1,27 @@
+(*:wrap=hard:maxLineLen=78:*)
+
 theory Presentation
 imports Base
 begin
 
 chapter \<open>Presenting theories \label{ch:present}\<close>
 
-text \<open>Isabelle provides several ways to present the outcome of
-  formal developments, including WWW-based browsable libraries or
-  actual printable documents.  Presentation is centered around the
-  concept of \<^emph>\<open>sessions\<close> (\chref{ch:session}).  The global session
-  structure is that of a tree, with Isabelle Pure at its root, further
-  object-logics derived (e.g.\ HOLCF from HOL, and HOL from Pure), and
-  application sessions further on in the hierarchy.
+text \<open>
+  Isabelle provides several ways to present the outcome of formal
+  developments, including WWW-based browsable libraries or actual printable
+  documents. Presentation is centered around the concept of \<^emph>\<open>sessions\<close>
+  (\chref{ch:session}). The global session structure is that of a tree, with
+  Isabelle Pure at its root, further object-logics derived (e.g.\ HOLCF from
+  HOL, and HOL from Pure), and application sessions further on in the
+  hierarchy.
 
-  The tools @{tool_ref mkroot} and @{tool_ref build} provide the
-  primary means for managing Isabelle sessions, including proper setup
-  for presentation; @{tool build} takes care to have @{executable_ref
-  "isabelle_process"} run any additional stages required for document
-  preparation, notably the @{tool_ref document} and @{tool_ref latex}.
-  The complete tool chain for managing batch-mode Isabelle sessions is
-  illustrated in \figref{fig:session-tools}.
+  The tools @{tool_ref mkroot} and @{tool_ref build} provide the primary means
+  for managing Isabelle sessions, including proper setup for presentation;
+  @{tool build} takes care to have @{executable_ref "isabelle_process"} run
+  any additional stages required for document preparation, notably the
+  @{tool_ref document} and @{tool_ref latex}. The complete tool chain for
+  managing batch-mode Isabelle sessions is illustrated in
+  \figref{fig:session-tools}.
 
   \begin{figure}[htbp]
   \begin{center}
@@ -53,58 +56,55 @@
 text \<open>
   \index{theory browsing information|bold}
 
-  As a side-effect of building sessions, Isabelle is able to generate
-  theory browsing information, including HTML documents that show the
-  theory sources and the relationship with its ancestors and
-  descendants.  Besides the HTML file that is generated for every
-  theory, Isabelle stores links to all theories of a session in an
-  index file.  As a second hierarchy, groups of sessions are organized
-  as \<^emph>\<open>chapters\<close>, with a separate index.  Note that the implicit
-  tree structure of the session build hierarchy is \<^emph>\<open>not\<close> relevant
+  As a side-effect of building sessions, Isabelle is able to generate theory
+  browsing information, including HTML documents that show the theory sources
+  and the relationship with its ancestors and descendants. Besides the HTML
+  file that is generated for every theory, Isabelle stores links to all
+  theories of a session in an index file. As a second hierarchy, groups of
+  sessions are organized as \<^emph>\<open>chapters\<close>, with a separate index. Note that the
+  implicit tree structure of the session build hierarchy is \<^emph>\<open>not\<close> relevant
   for the presentation.
 
-  Isabelle also generates graph files that represent the theory
-  dependencies within a session.  There is a graph browser Java applet
-  embedded in the generated HTML pages, and also a stand-alone
-  application that allows browsing theory graphs without having to
-  start a WWW client first.  The latter version also includes features
-  such as generating Postscript files, which are not available in the
-  applet version.  See \secref{sec:browse} for further information.
+  Isabelle also generates graph files that represent the theory dependencies
+  within a session. There is a graph browser Java applet embedded in the
+  generated HTML pages, and also a stand-alone application that allows
+  browsing theory graphs without having to start a WWW client first. The
+  latter version also includes features such as generating Postscript files,
+  which are not available in the applet version. See \secref{sec:browse} for
+  further information.
 
   \<^medskip>
-  The easiest way to let Isabelle generate theory browsing information
-  for existing sessions is to invoke @{tool build} with suitable
-  options:
+  The easiest way to let Isabelle generate theory browsing information for
+  existing sessions is to invoke @{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 \<^verbatim>\<open>$ISABELLE_BROWSER_INFO/FOL/FOL\<close> as
+  reported by the above verbose invocation of the build process.
 
   Many Isabelle sessions (such as \<^verbatim>\<open>HOL-Library\<close> in @{file
-  "~~/src/HOL/Library"}) also provide actual printable documents.
-  These are prepared automatically as well if enabled like this:
+  "~~/src/HOL/Library"}) also provide actual printable documents. These are
+  prepared automatically as well if enabled like this:
   @{verbatim [display] \<open>isabelle build -o browser_info -o document=pdf -v -c HOL-Library\<close>}
 
-  Enabling both browser info and document preparation simultaneously
-  causes an appropriate ``document'' link to be included in the HTML
-  index.  Documents may be generated independently of browser
-  information as well, see \secref{sec:tool-document} for further
-  details.
+  Enabling both browser info and document preparation simultaneously causes an
+  appropriate ``document'' link to be included in the HTML index. Documents
+  may be generated independently of browser information as well, see
+  \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.\<close>
+  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.
+\<close>
 
 
 section \<open>Preparing session root directories \label{sec:tool-mkroot}\<close>
 
-text \<open>The @{tool_def mkroot} tool configures a given directory as
-  session root, with some \<^verbatim>\<open>ROOT\<close> file and optional document
-  source directory.  Its usage is:
+text \<open>
+  The @{tool_def mkroot} tool configures a given directory as session root,
+  with some \<^verbatim>\<open>ROOT\<close> file and optional document source directory. Its usage is:
   @{verbatim [display]
 \<open>Usage: isabelle mkroot [OPTIONS] [DIR]
 
@@ -114,46 +114,45 @@
 
   Prepare session root DIR (default: current directory).\<close>}
 
-  The results are placed in the given directory \<open>dir\<close>, which
-  refers to the current directory by default.  The @{tool mkroot} tool
-  is conservative in the sense that it does not overwrite existing
-  files or directories.  Earlier attempts to generate a session root
-  need to be deleted manually.
+  The results are placed in the given directory \<open>dir\<close>, which refers to the
+  current directory by default. The @{tool mkroot} tool is conservative in the
+  sense that it does not overwrite existing files or directories. Earlier
+  attempts to generate a session root need to be deleted manually.
 
   \<^medskip>
-  Option \<^verbatim>\<open>-d\<close> indicates that the session shall be
-  accompanied by a formal document, with \<open>DIR\<close>\<^verbatim>\<open>/document/root.tex\<close>
-  as its {\LaTeX} entry point (see also \chref{ch:present}).
+  Option \<^verbatim>\<open>-d\<close> indicates that the session shall be accompanied by a formal
+  document, with \<open>DIR\<close>\<^verbatim>\<open>/document/root.tex\<close> as its {\LaTeX} entry point (see
+  also \chref{ch:present}).
 
-  Option \<^verbatim>\<open>-n\<close> allows to specify an alternative session
-  name; otherwise the base name of the given directory is used.
+  Option \<^verbatim>\<open>-n\<close> allows to specify an alternative session name; otherwise the
+  base name of the given directory is used.
 
   \<^medskip>
-  The implicit Isabelle settings variable @{setting
-  ISABELLE_LOGIC} specifies the parent session, and @{setting
-  ISABELLE_DOCUMENT_FORMAT} the document format to be filled filled
-  into the generated \<^verbatim>\<open>ROOT\<close> file.
+  The implicit Isabelle settings variable @{setting ISABELLE_LOGIC} specifies
+  the parent session, and @{setting ISABELLE_DOCUMENT_FORMAT} the document
+  format to be filled filled into the generated \<^verbatim>\<open>ROOT\<close> file.
 \<close>
 
 
 subsubsection \<open>Examples\<close>
 
-text \<open>Produce session \<^verbatim>\<open>Test\<close> (with document preparation)
-  within a separate directory of the same name:
+text \<open>
+  Produce session \<^verbatim>\<open>Test\<close> (with document preparation) within a separate
+  directory of the same name:
   @{verbatim [display] \<open>isabelle mkroot -d Test && isabelle build -D Test\<close>}
 
   \<^medskip>
-  Upgrade the current directory into a session ROOT with
-  document preparation, and build it:
+  Upgrade the current directory into a session ROOT with document preparation,
+  and build it:
   @{verbatim [display] \<open>isabelle mkroot -d && isabelle build -D .\<close>}
 \<close>
 
 
 section \<open>Preparing Isabelle session documents \label{sec:tool-document}\<close>
 
-text \<open>The @{tool_def document} tool prepares logic session
-  documents, processing the sources as provided by the user and
-  generated by Isabelle.  Its usage is:
+text \<open>
+  The @{tool_def document} tool prepares logic session documents, processing
+  the sources as provided by the user and generated by Isabelle. Its usage is:
   @{verbatim [display]
 \<open>Usage: isabelle document [OPTIONS] [DIR]
 
@@ -168,90 +167,83 @@
 
   This tool is usually run automatically as part of the Isabelle build
   process, provided document preparation has been enabled via suitable
-  options.  It may be manually invoked on the generated browser
-  information document output as well, e.g.\ in case of errors
-  encountered in the batch run.
+  options. It may be manually invoked on the generated browser information
+  document output as well, e.g.\ in case of errors encountered in the batch
+  run.
 
   \<^medskip>
-  The \<^verbatim>\<open>-c\<close> option tells @{tool document} to
-  dispose the document sources after successful operation!  This is
-  the right thing to do for sources generated by an Isabelle process,
-  but take care of your files in manual document preparation!
+  The \<^verbatim>\<open>-c\<close> option tells @{tool document} to dispose the document sources
+  after successful operation! This is the right thing to do for sources
+  generated by an Isabelle process, but take care of your files in manual
+  document preparation!
 
   \<^medskip>
-  The \<^verbatim>\<open>-n\<close> and \<^verbatim>\<open>-o\<close> option specify
-  the final output file name and format, the default is ``\<^verbatim>\<open>document.dvi\<close>''.
-  Note that the result will appear in the parent of the target \<^verbatim>\<open>DIR\<close>.
+  The \<^verbatim>\<open>-n\<close> and \<^verbatim>\<open>-o\<close> option specify the final output file name and format,
+  the default is ``\<^verbatim>\<open>document.dvi\<close>''. Note that the result will appear in the
+  parent of the target \<^verbatim>\<open>DIR\<close>.
 
   \<^medskip>
-  The \<^verbatim>\<open>-t\<close> option tells {\LaTeX} how to interpret
-  tagged Isabelle command regions.  Tags are specified as a comma
-  separated list of modifier/name pairs: ``\<^verbatim>\<open>+\<close>\<open>foo\<close>'' (or just ``\<open>foo\<close>'')
-  means to keep, ``\<^verbatim>\<open>-\<close>\<open>foo\<close>'' to drop, and ``\<^verbatim>\<open>/\<close>\<open>foo\<close>'' to
-  fold text tagged as \<open>foo\<close>.  The builtin default is equivalent
-  to the tag specification ``\<^verbatim>\<open>+theory,+proof,+ML,+visible,-invisible\<close>'';
-  see also the {\LaTeX} macros \<^verbatim>\<open>\isakeeptag\<close>, \<^verbatim>\<open>\isadroptag\<close>, and
-  \<^verbatim>\<open>\isafoldtag\<close>, in @{file "~~/lib/texinputs/isabelle.sty"}.
+  The \<^verbatim>\<open>-t\<close> option tells {\LaTeX} how to interpret tagged Isabelle command
+  regions. Tags are specified as a comma separated list of modifier/name
+  pairs: ``\<^verbatim>\<open>+\<close>\<open>foo\<close>'' (or just ``\<open>foo\<close>'') means to keep, ``\<^verbatim>\<open>-\<close>\<open>foo\<close>'' to
+  drop, and ``\<^verbatim>\<open>/\<close>\<open>foo\<close>'' to fold text tagged as \<open>foo\<close>. The builtin default is
+  equivalent to the tag specification
+  ``\<^verbatim>\<open>+theory,+proof,+ML,+visible,-invisible\<close>''; see also the {\LaTeX} macros
+  \<^verbatim>\<open>\isakeeptag\<close>, \<^verbatim>\<open>\isadroptag\<close>, and \<^verbatim>\<open>\isafoldtag\<close>, in @{file
+  "~~/lib/texinputs/isabelle.sty"}.
 
   \<^medskip>
-  Document preparation requires a \<^verbatim>\<open>document\<close>
-  directory within the session sources.  This directory is supposed to
-  contain all the files needed to produce the final document --- apart
-  from the actual theories which are generated by Isabelle.
+  Document preparation requires a \<^verbatim>\<open>document\<close> directory within the session
+  sources. This directory is supposed to contain all the files needed to
+  produce the final document --- apart from the actual theories which are
+  generated by Isabelle.
 
   \<^medskip>
-  For most practical purposes, @{tool document} is smart
-  enough to create any of the specified output formats, taking
-  \<^verbatim>\<open>root.tex\<close> supplied by the user as a starting point.  This
-  even includes multiple runs of {\LaTeX} to accommodate references
-  and bibliographies (the latter assumes \<^verbatim>\<open>root.bib\<close> within
-  the same directory).
+  For most practical purposes, @{tool document} is smart enough to create any
+  of the specified output formats, taking \<^verbatim>\<open>root.tex\<close> supplied by the user as
+  a starting point. This even includes multiple runs of {\LaTeX} to
+  accommodate references and bibliographies (the latter assumes \<^verbatim>\<open>root.bib\<close>
+  within the same directory).
 
-  In more complex situations, a separate \<^verbatim>\<open>build\<close> script for
-  the document sources may be given.  It is invoked with command-line
-  arguments for the document format and the document variant name.
-  The script needs to produce corresponding output files, e.g.\
-  \<^verbatim>\<open>root.pdf\<close> for target format \<^verbatim>\<open>pdf\<close> (and default
-  variants).  The main work can be again delegated to @{tool latex},
-  but it is also possible to harvest generated {\LaTeX} sources and
-  copy them elsewhere.
+  In more complex situations, a separate \<^verbatim>\<open>build\<close> script for the document
+  sources may be given. It is invoked with command-line arguments for the
+  document format and the document variant name. The script needs to produce
+  corresponding output files, e.g.\ \<^verbatim>\<open>root.pdf\<close> for target format \<^verbatim>\<open>pdf\<close> (and
+  default variants). The main work can be again delegated to @{tool latex},
+  but it is also possible to harvest generated {\LaTeX} sources and copy them
+  elsewhere.
 
   \<^medskip>
-  When running the session, Isabelle copies the content of
-  the original \<^verbatim>\<open>document\<close> directory into its proper place
-  within @{setting ISABELLE_BROWSER_INFO}, according to the session
-  path and document variant.  Then, for any processed theory \<open>A\<close>
-  some {\LaTeX} source is generated and put there as \<open>A\<close>\<^verbatim>\<open>.tex\<close>.
-  Furthermore, a list of all generated theory
-  files is put into \<^verbatim>\<open>session.tex\<close>.  Typically, the root
-  {\LaTeX} file provided by the user would include \<^verbatim>\<open>session.tex\<close>
-  to get a document containing all the theories.
+  When running the session, Isabelle copies the content of the original
+  \<^verbatim>\<open>document\<close> directory into its proper place within @{setting
+  ISABELLE_BROWSER_INFO}, according to the session path and document variant.
+  Then, for any processed theory \<open>A\<close> some {\LaTeX} source is generated and put
+  there as \<open>A\<close>\<^verbatim>\<open>.tex\<close>. Furthermore, a list of all generated theory files is
+  put into \<^verbatim>\<open>session.tex\<close>. Typically, the root {\LaTeX} file provided by the
+  user would include \<^verbatim>\<open>session.tex\<close> to get a document containing all the
+  theories.
 
-  The {\LaTeX} versions of the theories require some macros defined in
-  @{file "~~/lib/texinputs/isabelle.sty"}.  Doing \<^verbatim>\<open>\usepackage{isabelle}\<close>
-  in \<^verbatim>\<open>root.tex\<close> should be fine; the underlying @{tool latex} already
-  includes an appropriate path specification for {\TeX} inputs.
+  The {\LaTeX} versions of the theories require some macros defined in @{file
+  "~~/lib/texinputs/isabelle.sty"}. Doing \<^verbatim>\<open>\usepackage{isabelle}\<close> in
+  \<^verbatim>\<open>root.tex\<close> should be fine; the underlying @{tool latex} already includes an
+  appropriate path specification for {\TeX} inputs.
 
-  If the text contains any references to Isabelle symbols (such as
-  \<^verbatim>\<open>\<forall>\<close>) then \<^verbatim>\<open>isabellesym.sty\<close> should be included as well.
-  This package contains a standard set of {\LaTeX} macro definitions
-  \<^verbatim>\<open>\isasym\<close>\<open>foo\<close> corresponding to \<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>foo\<close>\<^verbatim>\<open>>\<close>,
-  see @{cite "isabelle-implementation"} for a
-  complete list of predefined Isabelle symbols.  Users may invent
-  further symbols as well, just by providing {\LaTeX} macros in a
-  similar fashion as in @{file "~~/lib/texinputs/isabellesym.sty"} of
-  the Isabelle distribution.
+  If the text contains any references to Isabelle symbols (such as \<^verbatim>\<open>\<forall>\<close>) then
+  \<^verbatim>\<open>isabellesym.sty\<close> should be included as well. This package contains a
+  standard set of {\LaTeX} macro definitions \<^verbatim>\<open>\isasym\<close>\<open>foo\<close> corresponding to
+  \<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>foo\<close>\<^verbatim>\<open>>\<close>, see @{cite "isabelle-implementation"} for a complete list
+  of predefined Isabelle symbols. Users may invent further symbols as well,
+  just by providing {\LaTeX} macros in a similar fashion as in @{file
+  "~~/lib/texinputs/isabellesym.sty"} of the Isabelle distribution.
 
-  For proper setup of DVI and PDF documents (with hyperlinks and
-  bookmarks), we recommend to include @{file
-  "~~/lib/texinputs/pdfsetup.sty"} as well.
+  For proper setup of DVI and PDF documents (with hyperlinks and bookmarks),
+  we recommend to include @{file "~~/lib/texinputs/pdfsetup.sty"} as well.
 
   \<^medskip>
-  As a final step of Isabelle document preparation, @{tool
-  document}~\<^verbatim>\<open>-c\<close> is run on the resulting copy of the
-  \<^verbatim>\<open>document\<close> directory.  Thus the actual output document is
-  built and installed in its proper place.  The generated sources are
-  deleted after successful run of {\LaTeX} and friends.
+  As a final step of Isabelle document preparation, @{tool document}~\<^verbatim>\<open>-c\<close> is
+  run on the resulting copy of the \<^verbatim>\<open>document\<close> directory. Thus the actual
+  output document is built and installed in its proper place. The generated
+  sources are deleted after successful run of {\LaTeX} and friends.
 
   Some care is needed if the document output location is configured
   differently, say within a directory whose content is still required
@@ -262,8 +254,9 @@
 section \<open>Running {\LaTeX} within the Isabelle environment
   \label{sec:tool-latex}\<close>
 
-text \<open>The @{tool_def latex} tool provides the basic interface for
-  Isabelle document preparation.  Its usage is:
+text \<open>
+  The @{tool_def latex} tool provides the basic interface for Isabelle
+  document preparation. Its usage is:
   @{verbatim [display]
 \<open>Usage: isabelle latex [OPTIONS] [FILE]
 
@@ -274,32 +267,30 @@
   Run LaTeX (and related tools) on FILE (default root.tex),
   producing the specified output format.\<close>}
 
-  Appropriate {\LaTeX}-related programs are run on the input file,
-  according to the given output format: @{executable latex},
-  @{executable pdflatex}, @{executable dvips}, @{executable bibtex}
-  (for \<^verbatim>\<open>bbl\<close>), and @{executable makeindex} (for \<^verbatim>\<open>idx\<close>).
-  The actual commands are determined from the settings
-  environment (@{setting ISABELLE_PDFLATEX} etc.).
+  Appropriate {\LaTeX}-related programs are run on the input file, according
+  to the given output format: @{executable latex}, @{executable pdflatex},
+  @{executable dvips}, @{executable bibtex} (for \<^verbatim>\<open>bbl\<close>), and @{executable
+  makeindex} (for \<^verbatim>\<open>idx\<close>). The actual commands are determined from the
+  settings environment (@{setting ISABELLE_PDFLATEX} etc.).
 
-  The \<^verbatim>\<open>sty\<close> output format causes the Isabelle style files to
-  be updated from the distribution.  This is useful in special
-  situations where the document sources are to be processed another
-  time by separate tools.
+  The \<^verbatim>\<open>sty\<close> output format causes the Isabelle style files to be updated from
+  the distribution. This is useful in special situations where the document
+  sources are to be processed another time by separate tools.
 
-  The \<^verbatim>\<open>syms\<close> output is for internal use; it generates lists
-  of symbols that are available without loading additional {\LaTeX}
-  packages.
+  The \<^verbatim>\<open>syms\<close> output is for internal use; it generates lists of symbols that
+  are available without loading additional {\LaTeX} packages.
 \<close>
 
 
 subsubsection \<open>Examples\<close>
 
-text \<open>Invoking @{tool latex} by hand may be occasionally useful when
-  debugging failed attempts of the automatic document preparation
-  stage of batch-mode Isabelle.  The abortive process leaves the
-  sources at a certain place within @{setting ISABELLE_BROWSER_INFO},
-  see the runtime error message for details.  This enables users to
-  inspect {\LaTeX} runs in further detail, e.g.\ like this:
+text \<open>
+  Invoking @{tool latex} by hand may be occasionally useful when debugging
+  failed attempts of the automatic document preparation stage of batch-mode
+  Isabelle. The abortive process leaves the sources at a certain place within
+  @{setting ISABELLE_BROWSER_INFO}, see the runtime error message for details.
+  This enables users to inspect {\LaTeX} runs in further detail, e.g.\ like
+  this:
 
   @{verbatim [display]
 \<open>cd "$(isabelle getenv -b ISABELLE_BROWSER_INFO)/Unsorted/Test/document"
diff -r e717f152d2a8 -r f18f6e51e901 src/Doc/System/Scala.thy
--- a/src/Doc/System/Scala.thy	Wed Nov 04 19:52:38 2015 +0100
+++ b/src/Doc/System/Scala.thy	Wed Nov 04 20:18:46 2015 +0100
@@ -1,43 +1,47 @@
+(*:wrap=hard:maxLineLen=78:*)
+
 theory Scala
 imports Base
 begin
 
 chapter \<open>Isabelle/Scala development tools\<close>
 
-text \<open>Isabelle/ML and Isabelle/Scala are the two main language
-environments for Isabelle tool implementations.  There are some basic
-command-line tools to work with the underlying Java Virtual Machine,
-the Scala toplevel and compiler.  Note that Isabelle/jEdit
-@{cite "isabelle-jedit"} provides a Scala Console for interactive
-experimentation within the running application.\<close>
+text \<open>
+  Isabelle/ML and Isabelle/Scala are the two main language environments for
+  Isabelle tool implementations. There are some basic command-line tools to
+  work with the underlying Java Virtual Machine, the Scala toplevel and
+  compiler. Note that Isabelle/jEdit @{cite "isabelle-jedit"} provides a Scala
+  Console for interactive experimentation within the running application.
+\<close>
 
 
 section \<open>Java Runtime Environment within Isabelle \label{sec:tool-java}\<close>
 
-text \<open>The @{tool_def java} tool is a direct wrapper for the Java
-  Runtime Environment, within the regular Isabelle settings
-  environment (\secref{sec:settings}).  The command line arguments are
-  that of the underlying Java version.  It is run in \<^verbatim>\<open>-server\<close> mode
-  if possible, to improve performance (at the cost of extra startup time).
+text \<open>
+  The @{tool_def java} tool is a direct wrapper for the Java Runtime
+  Environment, within the regular Isabelle settings environment
+  (\secref{sec:settings}). The command line arguments are that of the
+  underlying Java version. It is run in \<^verbatim>\<open>-server\<close> mode if possible, to
+  improve performance (at the cost of extra startup time).
 
-  The \<^verbatim>\<open>java\<close> executable is the one within @{setting
-  ISABELLE_JDK_HOME}, according to the standard directory layout for
-  official JDK distributions.  The class loader is augmented such that
-  the name space of \<^verbatim>\<open>Isabelle/Pure.jar\<close> is available,
-  which is the main Isabelle/Scala module.
+  The \<^verbatim>\<open>java\<close> executable is the one within @{setting ISABELLE_JDK_HOME},
+  according to the standard directory layout for official JDK distributions.
+  The class loader is augmented such that the name space of
+  \<^verbatim>\<open>Isabelle/Pure.jar\<close> is available, which is the main Isabelle/Scala module.
 
-  For example, the following command-line invokes the main method of
-  class \<^verbatim>\<open>isabelle.GUI_Setup\<close>, which opens a windows with
-  some diagnostic information about the Isabelle environment:
+  For example, the following command-line invokes the main method of class
+  \<^verbatim>\<open>isabelle.GUI_Setup\<close>, which opens a windows with some diagnostic
+  information about the Isabelle environment:
   @{verbatim [display] \<open>isabelle java isabelle.GUI_Setup\<close>}
 \<close>
 
 
 section \<open>Scala toplevel \label{sec:tool-scala}\<close>
 
-text \<open>The @{tool_def scala} tool is a direct wrapper for the Scala
-  toplevel; see also @{tool java} above.  The command line arguments
-  are that of the underlying Scala version.
+text \<open>
+  The @{tool_def scala} tool is a direct wrapper for the Scala toplevel; see
+  also @{tool java} above. The command line arguments are that of the
+  underlying Scala version.
 
   This allows to interact with Isabelle/Scala in TTY mode like this:
   @{verbatim [display]
@@ -51,32 +55,33 @@
 
 section \<open>Scala compiler \label{sec:tool-scalac}\<close>
 
-text \<open>The @{tool_def scalac} tool is a direct wrapper for the Scala
-  compiler; see also @{tool scala} above.  The command line arguments
-  are that of the underlying Scala version.
+text \<open>
+  The @{tool_def scalac} tool is a direct wrapper for the Scala compiler; see
+  also @{tool scala} above. The command line arguments are that of the
+  underlying Scala version.
 
   This allows to compile further Scala modules, depending on existing
-  Isabelle/Scala functionality.  The resulting class or jar files can
-  be added to the Java classpath using the \<^verbatim>\<open>classpath\<close> Bash
-  function that is provided by the Isabelle process environment.  Thus
-  add-on components can register themselves in a modular manner, see
-  also \secref{sec:components}.
+  Isabelle/Scala functionality. The resulting class or jar files can be added
+  to the Java classpath using the \<^verbatim>\<open>classpath\<close> Bash function that is provided
+  by the Isabelle process environment. Thus add-on components can register
+  themselves in a modular manner, see also \secref{sec:components}.
 
-  Note that jEdit @{cite "isabelle-jedit"} has its own mechanisms for
-  adding plugin components, which needs special attention since
-  it overrides the standard Java class loader.\<close>
+  Note that jEdit @{cite "isabelle-jedit"} has its own mechanisms for adding
+  plugin components, which needs special attention since it overrides the
+  standard Java class loader.
+\<close>
 
 
 section \<open>Scala script wrapper\<close>
 
-text \<open>The executable @{executable
-  "$ISABELLE_HOME/bin/isabelle_scala_script"} allows to run
-  Isabelle/Scala source files stand-alone programs, by using a
+text \<open>
+  The executable @{executable "$ISABELLE_HOME/bin/isabelle_scala_script"}
+  allows to run Isabelle/Scala source files stand-alone programs, by using a
   suitable ``hash-bang'' line and executable file permissions.
 
-  The subsequent example assumes that the main Isabelle binaries have
-  been installed in some directory that is included in @{setting PATH}
-  (see also @{tool "install"}):
+  The subsequent example assumes that the main Isabelle binaries have been
+  installed in some directory that is included in @{setting PATH} (see also
+  @{tool "install"}):
   @{verbatim [display]
 \<open>#!/usr/bin/env isabelle_scala_script
 
@@ -84,8 +89,8 @@
 Console.println("browser_info = " + options.bool("browser_info"))
 Console.println("document = " + options.string("document"))\<close>}
 
-  Alternatively the full @{file
-  "$ISABELLE_HOME/bin/isabelle_scala_script"} may be specified in
-  expanded form.\<close>
+  Alternatively the full @{file "$ISABELLE_HOME/bin/isabelle_scala_script"}
+  may be specified in expanded form.
+\<close>
 
 end
diff -r e717f152d2a8 -r f18f6e51e901 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Wed Nov 04 19:52:38 2015 +0100
+++ b/src/Doc/System/Sessions.thy	Wed Nov 04 20:18:46 2015 +0100
@@ -1,52 +1,52 @@
+(*:wrap=hard:maxLineLen=78:*)
+
 theory Sessions
 imports Base
 begin
 
 chapter \<open>Isabelle sessions and build management \label{ch:session}\<close>
 
-text \<open>An Isabelle \<^emph>\<open>session\<close> consists of a collection of related
-  theories that may be associated with formal documents
-  (\chref{ch:present}).  There is also a notion of \<^emph>\<open>persistent
-  heap\<close> image to capture the state of a session, similar to
-  object-code in compiled programming languages.  Thus the concept of
-  session resembles that of a ``project'' in common IDE environments,
-  but the specific name emphasizes the connection to interactive
-  theorem proving: the session wraps-up the results of
-  user-interaction with the prover in a persistent form.
+text \<open>
+  An Isabelle \<^emph>\<open>session\<close> consists of a collection of related theories that may
+  be associated with formal documents (\chref{ch:present}). There is also a
+  notion of \<^emph>\<open>persistent heap\<close> image to capture the state of a session,
+  similar to object-code in compiled programming languages. Thus the concept
+  of session resembles that of a ``project'' in common IDE environments, but
+  the specific name emphasizes the connection to interactive theorem proving:
+  the session wraps-up the results of user-interaction with the prover in a
+  persistent form.
 
-  Application sessions are built on a given parent session, which may
-  be built recursively on other parents.  Following this path in the
-  hierarchy eventually leads to some major object-logic session like
-  \<open>HOL\<close>, which itself is based on \<open>Pure\<close> as the common
-  root of all sessions.
+  Application sessions are built on a given parent session, which may be built
+  recursively on other parents. Following this path in the hierarchy
+  eventually leads to some major object-logic session like \<open>HOL\<close>, which itself
+  is based on \<open>Pure\<close> as the common root of all sessions.
 
-  Processing sessions may take considerable time.  Isabelle build
-  management helps to organize this efficiently.  This includes
-  support for parallel build jobs, in addition to the multithreaded
-  theory and proof checking that is already provided by the prover
-  process itself.\<close>
+  Processing sessions may take considerable time. Isabelle build management
+  helps to organize this efficiently. This includes support for parallel build
+  jobs, in addition to the multithreaded theory and proof checking that is
+  already provided by the prover process itself.
+\<close>
 
 
 section \<open>Session ROOT specifications \label{sec:session-root}\<close>
 
-text \<open>Session specifications reside in files called \<^verbatim>\<open>ROOT\<close>
-  within certain directories, such as the home locations of registered
-  Isabelle components or additional project directories given by the
-  user.
+text \<open>
+  Session specifications reside in files called \<^verbatim>\<open>ROOT\<close> within certain
+  directories, such as the home locations of registered Isabelle components or
+  additional project directories given by the user.
 
-  The ROOT file format follows the lexical conventions of the
-  \<^emph>\<open>outer syntax\<close> of Isabelle/Isar, see also
-  @{cite "isabelle-isar-ref"}.  This defines common forms like
-  identifiers, names, quoted strings, verbatim text, nested comments
-  etc.  The grammar for @{syntax session_chapter} and @{syntax
-  session_entry} is given as syntax diagram below; each ROOT file may
-  contain multiple specifications like this.  Chapters help to
-  organize browser info (\secref{sec:info}), but have no formal
-  meaning.  The default chapter is ``\<open>Unsorted\<close>''.
+  The ROOT file format follows the lexical conventions of the \<^emph>\<open>outer syntax\<close>
+  of Isabelle/Isar, see also @{cite "isabelle-isar-ref"}. This defines common
+  forms like identifiers, names, quoted strings, verbatim text, nested
+  comments etc. The grammar for @{syntax session_chapter} and @{syntax
+  session_entry} is given as syntax diagram below; each ROOT file may contain
+  multiple specifications like this. Chapters help to organize browser info
+  (\secref{sec:info}), but have no formal meaning. The default chapter is
+  ``\<open>Unsorted\<close>''.
 
-  Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple editing
-  mode \<^verbatim>\<open>isabelle-root\<close> for session ROOT files, which is
-  enabled by default for any file of that name.
+  Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple editing mode
+  \<^verbatim>\<open>isabelle-root\<close> for session ROOT files, which is enabled by default for any
+  file of that name.
 
   @{rail \<open>
     @{syntax_def session_chapter}: @'chapter' @{syntax name}
@@ -77,151 +77,138 @@
     document_files: @'document_files' ('(' dir ')')? (@{syntax name}+)
   \<close>}
 
-  \<^descr> \isakeyword{session}~\<open>A = B + body\<close> defines a new
-  session \<open>A\<close> based on parent session \<open>B\<close>, with its
-  content given in \<open>body\<close> (theories and auxiliary source files).
-  Note that a parent (like \<open>HOL\<close>) is mandatory in practical
+  \<^descr> \isakeyword{session}~\<open>A = B + body\<close> defines a new session \<open>A\<close> based on
+  parent session \<open>B\<close>, with its content given in \<open>body\<close> (theories and auxiliary
+  source files). Note that a parent (like \<open>HOL\<close>) is mandatory in practical
   applications: only Isabelle/Pure can bootstrap itself from nothing.
 
-  All such session specifications together describe a hierarchy (tree)
-  of sessions, with globally unique names.  The new session name
-  \<open>A\<close> should be sufficiently long and descriptive to stand on
-  its own in a potentially large library.
+  All such session specifications together describe a hierarchy (tree) of
+  sessions, with globally unique names. The new session name \<open>A\<close> should be
+  sufficiently long and descriptive to stand on its own in a potentially large
+  library.
 
-  \<^descr> \isakeyword{session}~\<open>A (groups)\<close> indicates a
-  collection of groups where the new session is a member.  Group names
-  are uninterpreted and merely follow certain conventions.  For
-  example, the Isabelle distribution tags some important sessions by
-  the group name called ``\<open>main\<close>''.  Other projects may invent
-  their own conventions, but this requires some care to avoid clashes
+  \<^descr> \isakeyword{session}~\<open>A (groups)\<close> indicates a collection of groups where
+  the new session is a member. Group names are uninterpreted and merely follow
+  certain conventions. For example, the Isabelle distribution tags some
+  important sessions by the group name called ``\<open>main\<close>''. Other projects may
+  invent their own conventions, but this requires some care to avoid clashes
   within this unchecked name space.
 
-  \<^descr> \isakeyword{session}~\<open>A\<close>~\isakeyword{in}~\<open>dir\<close>
-  specifies an explicit directory for this session; by default this is
-  the current directory of the \<^verbatim>\<open>ROOT\<close> file.
+  \<^descr> \isakeyword{session}~\<open>A\<close>~\isakeyword{in}~\<open>dir\<close> specifies an explicit
+  directory for this session; by default this is the current directory of the
+  \<^verbatim>\<open>ROOT\<close> file.
 
-  All theories and auxiliary source files are located relatively to
-  the session directory.  The prover process is run within the same as
-  its current working directory.
-
-  \<^descr> \isakeyword{description}~\<open>text\<close> is a free-form
-  annotation for this session.
+  All theories and auxiliary source files are located relatively to the
+  session directory. The prover process is run within the same as its current
+  working directory.
 
-  \<^descr> \isakeyword{options}~\<open>[x = a, y = b, z]\<close> defines
-  separate options (\secref{sec:system-options}) that are used when
-  processing this session, but \<^emph>\<open>without\<close> propagation to child
-  sessions.  Note that \<open>z\<close> abbreviates \<open>z = true\<close> for
-  Boolean options.
+  \<^descr> \isakeyword{description}~\<open>text\<close> is a free-form annotation for this
+  session.
 
-  \<^descr> \isakeyword{theories}~\<open>options names\<close> specifies a
-  block of theories that are processed within an environment that is
-  augmented by the given options, in addition to the global session
-  options given before.  Any number of blocks of \isakeyword{theories}
-  may be given.  Options are only active for each
+  \<^descr> \isakeyword{options}~\<open>[x = a, y = b, z]\<close> defines separate options
+  (\secref{sec:system-options}) that are used when processing this session,
+  but \<^emph>\<open>without\<close> propagation to child sessions. Note that \<open>z\<close> abbreviates \<open>z =
+  true\<close> for Boolean options.
+
+  \<^descr> \isakeyword{theories}~\<open>options names\<close> specifies a block of theories that
+  are processed within an environment that is augmented by the given options,
+  in addition to the global session options given before. Any number of blocks
+  of \isakeyword{theories} may be given. Options are only active for each
   \isakeyword{theories} block separately.
 
-  \<^descr> \isakeyword{files}~\<open>files\<close> lists additional source
-  files that are involved in the processing of this session.  This
-  should cover anything outside the formal content of the theory
-  sources.  In contrast, files that are loaded formally
-  within a theory, e.g.\ via @{command "ML_file"}, need not be
+  \<^descr> \isakeyword{files}~\<open>files\<close> lists additional source files that are involved
+  in the processing of this session. This should cover anything outside the
+  formal content of the theory sources. In contrast, files that are loaded
+  formally within a theory, e.g.\ via @{command "ML_file"}, need not be
   declared again.
 
-  \<^descr> \isakeyword{document_files}~\<open>(\<close>\isakeyword{in}~\<open>base_dir) files\<close> lists source files for document preparation,
-  typically \<^verbatim>\<open>.tex\<close> and \<^verbatim>\<open>.sty\<close> for {\LaTeX}.
-  Only these explicitly given files are copied from the base directory
-  to the document output directory, before formal document processing
-  is started (see also \secref{sec:tool-document}).  The local path
-  structure of the \<open>files\<close> is preserved, which allows to
-  reconstruct the original directory hierarchy of \<open>base_dir\<close>.
+  \<^descr> \isakeyword{document_files}~\<open>(\<close>\isakeyword{in}~\<open>base_dir) files\<close> lists
+  source files for document preparation, typically \<^verbatim>\<open>.tex\<close> and \<^verbatim>\<open>.sty\<close> for
+  {\LaTeX}. Only these explicitly given files are copied from the base
+  directory to the document output directory, before formal document
+  processing is started (see also \secref{sec:tool-document}). The local path
+  structure of the \<open>files\<close> is preserved, which allows to reconstruct the
+  original directory hierarchy of \<open>base_dir\<close>.
 
   \<^descr> \isakeyword{document_files}~\<open>files\<close> abbreviates
-  \isakeyword{document_files}~\<open>(\<close>\isakeyword{in}~\<open>document) files\<close>, i.e.\ document sources are taken from the base
-  directory \<^verbatim>\<open>document\<close> within the session root directory.
+  \isakeyword{document_files}~\<open>(\<close>\isakeyword{in}~\<open>document) files\<close>, i.e.\
+  document sources are taken from the base directory \<^verbatim>\<open>document\<close> within the
+  session root directory.
 \<close>
 
 
 subsubsection \<open>Examples\<close>
 
-text \<open>See @{file "~~/src/HOL/ROOT"} for a diversity of practically
-  relevant situations, although it uses relatively complex
-  quasi-hierarchic naming conventions like \<^verbatim>\<open>HOL-SPARK\<close>,
-  \<^verbatim>\<open>HOL-SPARK-Examples\<close>.  An alternative is to use
-  unqualified names that are relatively long and descriptive, as in
-  the Archive of Formal Proofs (@{url "http://afp.sourceforge.net"}), for
-  example.\<close>
+text \<open>
+  See @{file "~~/src/HOL/ROOT"} for a diversity of practically relevant
+  situations, although it uses relatively complex quasi-hierarchic naming
+  conventions like \<^verbatim>\<open>HOL-SPARK\<close>, \<^verbatim>\<open>HOL-SPARK-Examples\<close>. An alternative is to
+  use unqualified names that are relatively long and descriptive, as in the
+  Archive of Formal Proofs (@{url "http://afp.sourceforge.net"}), for
+  example.
+\<close>
 
 
 section \<open>System build options \label{sec:system-options}\<close>
 
-text \<open>See @{file "~~/etc/options"} for the main defaults provided by
-  the Isabelle distribution.  Isabelle/jEdit @{cite "isabelle-jedit"}
-  includes a simple editing mode \<^verbatim>\<open>isabelle-options\<close> for
-  this file-format.
+text \<open>
+  See @{file "~~/etc/options"} for the main defaults provided by the Isabelle
+  distribution. Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple
+  editing mode \<^verbatim>\<open>isabelle-options\<close> for this file-format.
 
-  The following options are particularly relevant to build Isabelle
-  sessions, in particular with document preparation
-  (\chref{ch:present}).
+  The following options are particularly relevant to build Isabelle sessions,
+  in particular with document preparation (\chref{ch:present}).
 
-  \<^item> @{system_option_def "browser_info"} controls output of HTML
-  browser info, see also \secref{sec:info}.
+    \<^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
-  format, see @{tool document} option \<^verbatim>\<open>-o\<close> in
-  \secref{sec:tool-document}.  In practice, the most relevant values
-  are \<^verbatim>\<open>document=false\<close> or \<^verbatim>\<open>document=pdf\<close>.
+    \<^item> @{system_option_def "document"} specifies the document output format,
+    see @{tool document} option \<^verbatim>\<open>-o\<close> in \secref{sec:tool-document}. In
+    practice, the most relevant values are \<^verbatim>\<open>document=false\<close> or
+    \<^verbatim>\<open>document=pdf\<close>.
 
-  \<^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
-  \secref{sec:info}.  See also @{tool mkroot}, which generates a
-  default configuration with output readily available to the author of
-  the document.
+    \<^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 \secref{sec:info}. See also @{tool mkroot}, which generates a
+    default configuration with output readily available to the author of the
+    document.
 
-  \<^item> @{system_option_def "document_variants"} specifies document
-  variants as a colon-separated list of \<open>name=tags\<close> entries,
-  corresponding to @{tool document} options \<^verbatim>\<open>-n\<close> and
-  \<^verbatim>\<open>-t\<close>.
+    \<^item> @{system_option_def "document_variants"} specifies document variants as
+    a colon-separated list of \<open>name=tags\<close> entries, corresponding to @{tool
+    document} options \<^verbatim>\<open>-n\<close> and \<^verbatim>\<open>-t\<close>.
 
-  For example, \<^verbatim>\<open>document_variants=document:outline=/proof,/ML\<close> indicates
-  two documents: the one called \<^verbatim>\<open>document\<close> with default tags,
-  and the other called \<^verbatim>\<open>outline\<close> where proofs and ML
-  sections are folded.
+    For example, \<^verbatim>\<open>document_variants=document:outline=/proof,/ML\<close> indicates
+    two documents: the one called \<^verbatim>\<open>document\<close> with default tags, and the other
+    called \<^verbatim>\<open>outline\<close> where proofs and ML sections are folded.
 
-  Document variant names are just a matter of conventions.  It is also
-  possible to use different document variant names (without tags) for
-  different document root entries, see also
-  \secref{sec:tool-document}.
+    Document variant names are just a matter of conventions. It is also
+    possible to use different document variant names (without tags) for
+    different document root entries, see also \secref{sec:tool-document}.
 
-  \<^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 manual adjustment (on the
-  command-line or within personal settings or preferences, not within
-  a session \<^verbatim>\<open>ROOT\<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
+    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 the subsequent theories to be processed.
-  Conditions are considered ``true'' if the corresponding environment
-  value is defined and non-empty.
+    \<^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 value is defined and non-empty.
 
-  For example, the \<^verbatim>\<open>condition=ISABELLE_FULL_TEST\<close> may be
-  used to guard extraordinary theories, which are meant to be enabled
-  explicitly via some shell prefix \<^verbatim>\<open>env ISABELLE_FULL_TEST=true\<close>
-  before invoking @{tool build}.
+    For example, the \<^verbatim>\<open>condition=ISABELLE_FULL_TEST\<close> may be used to guard
+    extraordinary theories, which are meant to be enabled explicitly via some
+    shell prefix \<^verbatim>\<open>env ISABELLE_FULL_TEST=true\<close> before invoking @{tool build}.
 
-  \<^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
-  processes that get out of control, even if there is a deadlock
-  without CPU time usage.
+    \<^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 processes that get out of control, even if there is
+    a deadlock without CPU time usage.
 
-
-  The @{tool_def options} tool prints Isabelle system options.  Its
+  The @{tool_def options} tool prints Isabelle system options. Its
   command-line usage is:
   @{verbatim [display]
 \<open>Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...]
@@ -235,31 +222,28 @@
   Report Isabelle system options, augmented by MORE_OPTIONS given as
   arguments NAME=VAL or NAME.\<close>}
 
-  The command line arguments provide additional system options of the
-  form \<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close> or \<open>name\<close>
-  for Boolean options.
+  The command line arguments provide additional system options of the form
+  \<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close> or \<open>name\<close> for Boolean options.
+
+  Option \<^verbatim>\<open>-b\<close> augments the implicit environment of system options by the ones
+  of @{setting ISABELLE_BUILD_OPTIONS}, cf.\ \secref{sec:tool-build}.
 
-  Option \<^verbatim>\<open>-b\<close> augments the implicit environment of system
-  options by the ones of @{setting ISABELLE_BUILD_OPTIONS}, cf.\
-  \secref{sec:tool-build}.
+  Option \<^verbatim>\<open>-g\<close> prints the value of the given option. Option \<^verbatim>\<open>-l\<close> lists all
+  options with their declaration and current value.
 
-  Option \<^verbatim>\<open>-g\<close> prints the value of the given option.
-  Option \<^verbatim>\<open>-l\<close> lists all options with their declaration and
-  current value.
-
-  Option \<^verbatim>\<open>-x\<close> specifies a file to export the result in
-  YXML format, instead of printing it in human-readable form.
+  Option \<^verbatim>\<open>-x\<close> specifies a file to export the result in YXML format, instead
+  of printing it in human-readable form.
 \<close>
 
 
 section \<open>Invoking the build process \label{sec:tool-build}\<close>
 
-text \<open>The @{tool_def build} tool invokes the build process for
-  Isabelle sessions.  It manages dependencies between sessions,
-  related sources of theories and auxiliary files, and target heap
-  images.  Accordingly, it runs instances of the prover process with
-  optional document preparation.  Its command-line usage
-  is:\<^footnote>\<open>Isabelle/Scala provides the same functionality via
+text \<open>
+  The @{tool_def build} tool invokes the build process for Isabelle sessions.
+  It manages dependencies between sessions, related sources of theories and
+  auxiliary files, and target heap images. Accordingly, it runs instances of
+  the prover process with optional document preparation. Its command-line
+  usage is:\<^footnote>\<open>Isabelle/Scala provides the same functionality via
   \<^verbatim>\<open>isabelle.Build.build\<close>.\<close>
   @{verbatim [display]
 \<open>Usage: isabelle build [OPTIONS] [SESSIONS ...]
@@ -291,98 +275,87 @@
   ML_OPTIONS="..."\<close>}
 
   \<^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
-  directories given via options \<^verbatim>\<open>-d\<close>~\<open>DIR\<close> on the
-  command line.  Each such directory may contain a session
+  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 directories given via options
+  \<^verbatim>\<open>-d\<close>~\<open>DIR\<close> on the command line. Each such directory may contain a session
   \<^verbatim>\<open>ROOT\<close> file with several session specifications.
 
-  Any session root directory may refer recursively to further
-  directories of the same kind, by listing them in a catalog file
-  \<^verbatim>\<open>ROOTS\<close> line-by-line.  This helps to organize large
-  collections of session specifications, or to make \<^verbatim>\<open>-d\<close>
-  command line options persistent (say within
+  Any session root directory may refer recursively to further directories of
+  the same kind, by listing them in a catalog file \<^verbatim>\<open>ROOTS\<close> line-by-line. This
+  helps to organize large collections of session specifications, or to make
+  \<^verbatim>\<open>-d\<close> command line options persistent (say within
   \<^verbatim>\<open>$ISABELLE_HOME_USER/ROOTS\<close>).
 
   \<^medskip>
-  The subset of sessions to be managed is determined via
-  individual \<open>SESSIONS\<close> given as command-line arguments, or
-  session groups that are given via one or more options \<^verbatim>\<open>-g\<close>~\<open>NAME\<close>.
-  Option \<^verbatim>\<open>-a\<close> selects all sessions.
-  The build tool takes session dependencies into account: the set of
-  selected sessions is completed by including all ancestors.
+  The subset of sessions to be managed is determined via individual \<open>SESSIONS\<close>
+  given as command-line arguments, or session groups that are given via one or
+  more options \<^verbatim>\<open>-g\<close>~\<open>NAME\<close>. Option \<^verbatim>\<open>-a\<close> 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>\<open>-x\<close>~\<open>NAME\<close> specify
-  sessions to be excluded. All descendents of excluded sessions are removed
-  from the selection as specified above. Option \<^verbatim>\<open>-X\<close> is
-  analogous to this, but excluded sessions are specified by session group
-  membership.
+  One or more options \<^verbatim>\<open>-x\<close>~\<open>NAME\<close> specify sessions to be excluded. All
+  descendents of excluded sessions are removed from the selection as specified
+  above. Option \<^verbatim>\<open>-X\<close> is analogous to this, but excluded sessions are
+  specified by session group membership.
 
   \<^medskip>
-  Option \<^verbatim>\<open>-R\<close> 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>\<open>-R\<close>).
+  Option \<^verbatim>\<open>-R\<close> 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>\<open>-R\<close>).
 
   \<^medskip>
-  Option \<^verbatim>\<open>-D\<close> is similar to \<^verbatim>\<open>-d\<close>, but
-  selects all sessions that are defined in the given directories.
+  Option \<^verbatim>\<open>-D\<close> is similar to \<^verbatim>\<open>-d\<close>, but selects all sessions that are defined
+  in the given directories.
 
   \<^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.\
-  \<^verbatim>\<open>ISABELLE_BUILD_OPTIONS="document=pdf threads=4"\<close>. Moreover,
-  the environment of system build options may be augmented on the
-  command line via \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close> or \<^verbatim>\<open>-o\<close>~\<open>name\<close>, which
-  abbreviates \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=true\<close> for
-  Boolean options.  Multiple occurrences of \<^verbatim>\<open>-o\<close> on the
-  command-line are applied in the given order.
+  (\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.\ \<^verbatim>\<open>ISABELLE_BUILD_OPTIONS="document=pdf
+  threads=4"\<close>. Moreover, the environment of system build options may be
+  augmented on the command line via \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close> or \<^verbatim>\<open>-o\<close>~\<open>name\<close>,
+  which abbreviates \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=true\<close> for Boolean options. Multiple
+  occurrences of \<^verbatim>\<open>-o\<close> on the command-line are applied in the given order.
 
   \<^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 of sessions, as required for
-  other sessions to continue later on.
+  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
+  of sessions, as required for other sessions to continue later on.
 
   \<^medskip>
-  Option \<^verbatim>\<open>-c\<close> cleans all descendants of the
-  selected sessions before performing the specified build operation.
+  Option \<^verbatim>\<open>-c\<close> cleans all descendants of the selected sessions before
+  performing the specified build operation.
 
   \<^medskip>
-  Option \<^verbatim>\<open>-n\<close> 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.
+  Option \<^verbatim>\<open>-n\<close> 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>\<open>-j\<close> 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}.
+  Option \<^verbatim>\<open>-j\<close> 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>\<open>-s\<close> enables \<^emph>\<open>system mode\<close>, 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).
+  Option \<^verbatim>\<open>-s\<close> enables \<^emph>\<open>system mode\<close>, 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>\<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. 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.\<close>
+  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.
+\<close>
 
 
 subsubsection \<open>Examples\<close>
@@ -396,23 +369,22 @@
   @{verbatim [display] \<open>isabelle build -b -g main\<close>}
 
   \<^smallskip>
-  Provide a general overview of the status of all Isabelle
-  sessions, without building anything:
+  Provide a general overview of the status of all Isabelle sessions, without
+  building anything:
   @{verbatim [display] \<open>isabelle build -a -n -v\<close>}
 
   \<^smallskip>
-  Build all sessions with HTML browser info and PDF
-  document preparation:
+  Build all sessions with HTML browser info and PDF document preparation:
   @{verbatim [display] \<open>isabelle build -a -o browser_info -o document=pdf\<close>}
 
   \<^smallskip>
-  Build all sessions with a maximum of 8 parallel prover
-  processes and 4 worker threads each (on a machine with many cores):
+  Build all sessions with a maximum of 8 parallel prover processes and 4
+  worker threads each (on a machine with many cores):
   @{verbatim [display] \<open>isabelle build -a -j8 -o threads=4\<close>}
 
   \<^smallskip>
-  Build some session images with cleanup of their
-  descendants, while retaining their ancestry:
+  Build some session images with cleanup of their descendants, while retaining
+  their ancestry:
   @{verbatim [display] \<open>isabelle build -b -c HOL-Algebra HOL-Word\<close>}
 
   \<^smallskip>
@@ -420,14 +392,14 @@
   @{verbatim [display] \<open>isabelle build -a -n -c\<close>}
 
   \<^smallskip>
-  Build all sessions from some other directory hierarchy,
-  according to the settings variable \<^verbatim>\<open>AFP\<close> that happens to
-  be defined inside the Isabelle environment:
+  Build all sessions from some other directory hierarchy, according to the
+  settings variable \<^verbatim>\<open>AFP\<close> that happens to be defined inside the Isabelle
+  environment:
   @{verbatim [display] \<open>isabelle build -D '$AFP'\<close>}
 
   \<^smallskip>
-  Inform about the status of all sessions required for AFP,
-  without building anything yet:
+  Inform about the status of all sessions required for AFP, without building
+  anything yet:
   @{verbatim [display] \<open>isabelle build -D '$AFP' -R -v -n\<close>}
 \<close>