--- a/src/Doc/System/Sessions.thy Wed Mar 13 15:08:38 2013 +0100
+++ b/src/Doc/System/Sessions.thy Wed Mar 13 15:12:14 2013 +0100
@@ -38,15 +38,20 @@
\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.
+ 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 ``@{text "Unsorted"}''.
Isabelle/jEdit (\secref{sec:tool-jedit}) includes a simple editing
mode @{verbatim "isabelle-root"} for session ROOT files, which is
enabled by default for any file of that name.
@{rail "
+ @{syntax_def session_chapter}: @'chapter' @{syntax name}
+ ;
+
@{syntax_def session_entry}: @'session' spec '=' (@{syntax name} '+')? body
;
body: description? options? ( theories + ) files?