diff -r 21361b6189a6 -r 0b95a13ed90a doc-src/System/Thy/Sessions.thy
--- 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} *}