1.1 --- a/src/Doc/System/Sessions.thy	Sat Jan 26 12:45:32 2013 +0100
     1.2 +++ b/src/Doc/System/Sessions.thy	Sat Jan 26 13:43:37 2013 +0100
     1.3 @@ -5,8 +5,8 @@
     1.4  chapter {* Isabelle sessions and build management \label{ch:session} *}
     1.5  
     1.6  text {* An Isabelle \emph{session} consists of a collection of related
     1.7 -  theories that may be associated with formal documents (see also
     1.8 -  \chref{ch:present}).  There is also a notion of \emph{persistent
     1.9 +  theories that may be associated with formal documents
    1.10 +  (\chref{ch:present}).  There is also a notion of \emph{persistent
    1.11    heap} image to capture the state of a session, similar to
    1.12    object-code in compiled programming languages.  Thus the concept of
    1.13    session resembles that of a ``project'' in common IDE environments,
    1.14 @@ -43,7 +43,8 @@
    1.15    specifications like this.
    1.16  
    1.17    Isabelle/jEdit (\secref{sec:tool-jedit}) includes a simple editing
    1.18 -  mode @{verbatim "isabelle-root"} for session ROOT files.
    1.19 +  mode @{verbatim "isabelle-root"} for session ROOT files, which is
    1.20 +  enabled by default for any file of that name.
    1.21  
    1.22    @{rail "
    1.23      @{syntax_def session_entry}: @'session' spec '=' (@{syntax name} '+')? body
    1.24 @@ -79,8 +80,8 @@
    1.25  
    1.26    All such session specifications together describe a hierarchy (tree)
    1.27    of sessions, with globally unique names.  The new session name
    1.28 -  @{text "A"} should be sufficiently long to stand on its own in a
    1.29 -  potentially large library.
    1.30 +  @{text "A"} should be sufficiently long and descriptive to stand on
    1.31 +  its own in a potentially large library.
    1.32  
    1.33    \item \isakeyword{session}~@{text "A (groups)"} indicates a
    1.34    collection of groups where the new session is a member.  Group names
    1.35 @@ -118,19 +119,20 @@
    1.36    files that are involved in the processing of this session.  This
    1.37    should cover anything outside the formal content of the theory
    1.38    sources, say some auxiliary {\TeX} files that are required for
    1.39 -  document processing.  In contrast, files that are specified in
    1.40 -  formal theory headers as @{keyword "uses"} need not be declared
    1.41 -  again.
    1.42 +  document processing.  In contrast, files that are loaded formally
    1.43 +  within a theory, e.g.\ via @{keyword "ML_file"}, need not be
    1.44 +  declared again.
    1.45  
    1.46    \end{description}
    1.47  *}
    1.48  
    1.49 +
    1.50  subsubsection {* Examples *}
    1.51  
    1.52  text {* See @{file "~~/src/HOL/ROOT"} for a diversity of practically
    1.53 -  relevant situations, but it uses relatively complex quasi-hierarchic
    1.54 -  naming conventions like @{text "HOL\<dash>SPARK"}, @{text
    1.55 -  "HOL\<dash>SPARK\<dash>Examples"}.  An alternative is to use
    1.56 +  relevant situations, although it uses relatively complex
    1.57 +  quasi-hierarchic naming conventions like @{text "HOL\<dash>SPARK"},
    1.58 +  @{text "HOL\<dash>SPARK\<dash>Examples"}.  An alternative is to use
    1.59    unqualified names that are relatively long and descriptive, as in
    1.60    the Archive of Formal Proofs (\url{http://afp.sf.net}), for
    1.61    example. *}
    1.62 @@ -143,6 +145,81 @@
    1.63    includes a simple editing mode @{verbatim "isabelle-options"} for
    1.64    this file-format.
    1.65  
    1.66 +  The following options are particulary relevant to build Isabelle
    1.67 +  sessions, in particular with document preparation
    1.68 +  (\chref{ch:present}).
    1.69 +
    1.70 +  \begin{itemize}
    1.71 +
    1.72 +  \item @{system_option_def "browser_info"} controls output of HTML
    1.73 +  browser info, see also \secref{sec:info}.
    1.74 +
    1.75 +  \item @{system_option_def "document"} specifies the document output
    1.76 +  format, see @{tool document} option @{verbatim "-o"} in
    1.77 +  \secref{sec:tool-document}.  In practice, the most relevant values
    1.78 +  are @{verbatim "document=false"} or @{verbatim "document=pdf"}.
    1.79 +
    1.80 +  \item @{system_option_def "document_output"} specifies an
    1.81 +  alternative directory for generated output of the document
    1.82 +  preparation system; the default is within the @{setting
    1.83 +  "ISABELLE_BROWSER_INFO"} hierarchy as explained in
    1.84 +  \secref{sec:info}.  See also @{tool mkroot}, which generates a
    1.85 +  default configuration with output readily available to the author of
    1.86 +  the document.
    1.87 +
    1.88 +  \item @{system_option_def "document_variants"} specifies document
    1.89 +  variants as a colon-separated list of @{text "name=tags"} entries,
    1.90 +  corresponding to @{tool document} options @{verbatim "-n"} and
    1.91 +  @{verbatim "-t"}.
    1.92 +
    1.93 +  For example, @{verbatim
    1.94 +  "document_variants=document:outline=/proof,/ML"} indicates two
    1.95 +  documents: the one called @{verbatim document} with default tags,
    1.96 +  and the other called @{verbatim outline} where proofs and ML
    1.97 +  sections are folded.
    1.98 +
    1.99 +  Document variant names are just a matter of conventions.  It is also
   1.100 +  possible to use different document variant names (without tags) for
   1.101 +  different document root entries, see also
   1.102 +  \secref{sec:tool-document}.
   1.103 +
   1.104 +  \item @{system_option_def "document_graph"} tells whether the
   1.105 +  generated document files should include a theory graph (cf.\
   1.106 +  \secref{sec:browse} and \secref{sec:info}).  The resulting EPS or
   1.107 +  PDF file can be included as graphics in {\LaTeX}.
   1.108 +
   1.109 +  Note that this option is usually determined as static parameter of
   1.110 +  some session (e.g.\ within its @{verbatim ROOT} file) and \emph{not}
   1.111 +  given globally or on the command line of @{tool build}.
   1.112 +
   1.113 +  \item @{system_option_def "threads"} determines the number of worker
   1.114 +  threads for parallel checking of theories and proofs.  The default
   1.115 +  @{text "0"} means that a sensible maximum value is determined by the
   1.116 +  underlying hardware.  For machines with many cores or with
   1.117 +  hyperthreading, this is often requires manual adjustment (on the
   1.118 +  command-line or within personal settings or preferences, not within
   1.119 +  a session @{verbatim ROOT}).
   1.120 +
   1.121 +  \item @{system_option_def "condition"} specifies a comma-separated
   1.122 +  list of process environment variables (or Isabelle settings) that
   1.123 +  are required for the subsequent theories to be processed.
   1.124 +  Conditions are considered ``true'' if the corresponding environment
   1.125 +  value is defined and non-empty.
   1.126 +
   1.127 +  For example, the @{verbatim "condition=ISABELLE_FULL_TEST"} may be
   1.128 +  used to guard extraordinary theories, which are meant to be enabled
   1.129 +  explicitly via some shell prefix @{verbatim "env ISABELLE_FULL_TEST=true"}
   1.130 +  before invoking @{tool build}.
   1.131 +
   1.132 +  \item @{system_option_def "timeout"} specifies a real wall-clock
   1.133 +  timeout (in seconds) for the session as a whole.  The timer is
   1.134 +  controlled outside the ML process by the JVM that runs
   1.135 +  Isabelle/Scala.  Thus it is relatively reliable in canceling
   1.136 +  processes that get out of control, even if there is a deadlock
   1.137 +  without CPU time usage.
   1.138 +
   1.139 +  \end{itemize}
   1.140 +
   1.141    The @{tool_def options} tool prints Isabelle system options.  Its
   1.142    command-line usage is:
   1.143  \begin{ttbox}