# HG changeset patch
# User wenzelm
# Date 1363183934 -3600
# Node ID d266f932936849c08d1f8b92c56679b68c2a24c2
# Parent  e2505a192a7c8ef20776180efdfe37cb2661a749
sessions may be organized via 'chapter' in ROOT;

diff -r e2505a192a7c -r d266f9329368 NEWS
--- a/NEWS	Wed Mar 13 15:08:38 2013 +0100
+++ b/NEWS	Wed Mar 13 15:12:14 2013 +0100
@@ -6,6 +6,13 @@
 
 *** General ***
 
+* Sessions may be organized via 'chapter' specifications in the ROOT
+file, which determines a two-level hierarchy of browser info.  The old
+tree-like organization via implicit sub-session relation, with its
+tendency towards erratic fluctuation of URLs, has been discontinued.
+The default chapter is "Unsorted".  Potential INCOMPATIBILITY for HTML
+presentation of theories.
+
 * Discontinued obsolete 'uses' within theory header.  Note that
 commands like 'ML_file' work without separate declaration of file
 dependencies.  Minor INCOMPATIBILITY.
diff -r e2505a192a7c -r d266f9329368 src/Doc/System/Presentation.thy
--- a/src/Doc/System/Presentation.thy	Wed Mar 13 15:08:38 2013 +0100
+++ b/src/Doc/System/Presentation.thy	Wed Mar 13 15:12:14 2013 +0100
@@ -57,9 +57,11 @@
   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 in an index
-  file. These indexes are linked with other indexes to represent the
-  overall tree structure of the sessions.
+  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{chapters}, with a separate index.  Note that the implicit
+  tree structure of the session build hierarchy is \emph{not} relevant
+  for the presentation.
 
   Isabelle also generates graph files that represent the theory
   dependencies within a session.  There is a graph browser Java applet
@@ -80,7 +82,7 @@
 \end{ttbox}
 
   The presentation output will appear in @{verbatim
-  "$ISABELLE_BROWSER_INFO/FOL"} as reported by the above verbose
+  "$ISABELLE_BROWSER_INFO/FOL/FOL"} as reported by the above verbose
   invocation of the build process.
 
   Many Isabelle sessions (such as @{verbatim "HOL-Library"} in @{file
@@ -99,11 +101,9 @@
   \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 identifier (according to the tree structure of sub-sessions
-  by default).  In order to present Isabelle applications on the web,
-  the corresponding subdirectory from @{setting ISABELLE_BROWSER_INFO}
-  can be put on a WWW server.
-*}
+  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.  *}
 
 section {* Preparing session root directories \label{sec:tool-mkroot} *}
 
@@ -311,7 +311,7 @@
   inspect {\LaTeX} runs in further detail, e.g.\ like this:
 
 \begin{ttbox}
-  cd ~/.isabelle/IsabelleXXXX/browser_info/HOL/Test/document
+  cd ~/.isabelle/IsabelleXXXX/browser_info/Unsorted/Test/document
   isabelle latex -o pdf
 \end{ttbox}
 *}
diff -r e2505a192a7c -r d266f9329368 src/Doc/System/Sessions.thy
--- 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?