--- a/doc-src/System/Thy/Sessions.thy Sat Jul 28 15:21:49 2012 +0200
+++ b/doc-src/System/Thy/Sessions.thy Sat Jul 28 18:20:47 2012 +0200
@@ -8,7 +8,116 @@
section {* Session ROOT specifications \label{sec:session-root} *}
-text {* FIXME *}
+text {* Session specifications reside in files called @{verbatim ROOT}
+ 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{outer syntax} 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 a single @{syntax session_entry} is given as
+ syntax diagram below; each ROOT file may contain multiple session
+ specifications like this.
+
+ Note that Isabelle/jEdit \secref{sec:tool-jedit} includes a simple
+ editing mode for session ROOT files.
+
+ @{rail "
+ @{syntax_def session_entry}: @'session' spec '=' (@{syntax name} '+')? body
+ ;
+ body: description? options? ( theories * ) files?
+ ;
+ spec: @{syntax name} '!'? groups? dir?
+ ;
+ groups: '(' (@{syntax name} +) ')'
+ ;
+ dir: @'in' @{syntax name}
+ ;
+ description: @'description' @{syntax text}
+ ;
+ options: @'options' opts
+ ;
+ opts: '[' ( (@{syntax name} '=' @{syntax name} | @{syntax name}) + ',' ) ']'
+ ;
+ theories: @'theories' opts? ( @{syntax name} + )
+ ;
+ files: @'files' ( @{syntax name} + )
+ "}
+
+ \begin{description}
+
+ \item \isakeyword{session}~@{text "A = B + body"} defines a new
+ session @{text "A"} based on parent session @{text "B"}, with its
+ content given in @{text body} (theories and auxiliary source files).
+ Note that a parent (like @{text "HOL"}) 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. By default, names are
+ derived from parent ones by concatenation, i.e.\ @{text "B\<dash>A"}
+ above. Cumulatively, this leads to session paths of the form @{text
+ "X\<dash>Y\<dash>Z\<dash>W"}. Note that in the specification,
+ @{text B} is already such a fully-qualified name, while @{text "A"}
+ is the new base name.
+
+ \item \isakeyword{session}~@{text "A! = B"} indicates a fresh start
+ in the naming scheme: the session is called just @{text "A"} instead
+ of @{text "B\<dash>A"}. Here the name @{text "A"} should be
+ sufficiently long to stand on its own in a potentially large
+ library.
+
+ \item \isakeyword{session}~@{text "A (groups)"} 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 @{text "main"}. Other projects may invent their own
+ conventions, which requires some care to avoid clashes within this
+ unchecked name space.
+
+ \item \isakeyword{session}~@{text "A"}~\isakeyword{in}~@{text "dir"}
+ specifies an explicit directory for this session. By default,
+ \isakeyword{session}~@{text "A"} abbreviates
+ \isakeyword{session}~@{text "A"}~\isakeyword{in}~@{text "A"}. This
+ accommodates the common scheme where some base directory contains
+ several sessions in sub-directories of corresponding names. Another
+ common scheme is \isakeyword{session}~@{text
+ "A"}~\isakeyword{in}~@{verbatim "\".\""} to refer to the current
+ directory of the ROOT 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.
+
+ \item \isakeyword{description}~@{text "text"} is a free-form
+ annotation for this session.
+
+ \item \isakeyword{options}~@{text "[x = a, y = b, z]"} defines
+ separate options that are used when processing this session, but
+ \emph{without} propagation to child sessions; see also
+ \secref{sec:system-options}. Note that @{text "z"} abbreviates
+ @{text "z = true"} for Boolean options.
+
+ \item \isakeyword{theories}~@{text "options names"} specifies a
+ block of theories that are processed within an environment that is
+ augmented further 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.
+
+ \item \isakeyword{files}~@{text "files"} lists additional source
+ files that are somehow involved in the processing of this session.
+ This should cover anything outside the formal content of the theory
+ sources, say some auxiliary {\TeX} files that are required for
+ document processing. In contrast, files that are specified in
+ formal theory headers as @{keyword "uses"} need not be declared
+ again.
+
+ \end{description}
+
+ Plenty of examples may be found in the Isabelle distribution, such
+ as in @{file "~~/src/HOL/ROOT"}. *}
section {* System build options \label{sec:system-options} *}