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