--- 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.
--- 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}
*}
--- 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?