1.1 --- a/src/Doc/IsarRef/Document_Preparation.thy	Sat Jan 26 13:49:48 2013 +0100
     1.2 +++ b/src/Doc/IsarRef/Document_Preparation.thy	Sat Jan 26 16:10:50 2013 +0100
     1.3 @@ -5,51 +5,17 @@
     1.4  chapter {* Document preparation \label{ch:document-prep} *}
     1.5  
     1.6  text {* Isabelle/Isar provides a simple document preparation system
     1.7 -  based on regular {PDF-\LaTeX} technology, with full support for
     1.8 -  hyper-links and bookmarks.  Thus the results are well suited for WWW
     1.9 -  browsing and as printed copies.
    1.10 +  based on regular {PDF-\LaTeX} technology, with support for
    1.11 +  hyper-links and bookmarks within that format.  Thus the results are
    1.12 +  well suited for WWW browsing and as printed copies.
    1.13  
    1.14 -  \medskip Isabelle generates {\LaTeX} output while running a
    1.15 -  \emph{logic session} (see also \cite{isabelle-sys}).  Getting
    1.16 -  started with a working configuration for common situations is quite
    1.17 -  easy by using the Isabelle @{verbatim mkdir} and @{verbatim make}
    1.18 -  tools.  First invoke
    1.19 -\begin{ttbox}
    1.20 -  isabelle mkdir Foo
    1.21 -\end{ttbox}
    1.22 -  to initialize a separate directory for session @{verbatim Foo} (it
    1.23 -  is safe to experiment, since @{verbatim "isabelle mkdir"} never
    1.24 -  overwrites existing files).  Ensure that @{verbatim "Foo/ROOT.ML"}
    1.25 -  holds ML commands to load all theories required for this session;
    1.26 -  furthermore @{verbatim "Foo/document/root.tex"} should include any
    1.27 -  special {\LaTeX} macro packages required for your document (the
    1.28 -  default is usually sufficient as a start).
    1.29 +  {\LaTeX} output is generated while processing a \emph{session} in
    1.30 +  batch mode, as explained in the \emph{The Isabelle System Manual}
    1.31 +  \cite{isabelle-sys}.  The main Isabelle tools to get started with
    1.32 +  document prepation are @{tool_ref mkroot} and @{tool_ref build}.
    1.33  
    1.34 -  The session is controlled by a separate @{verbatim IsaMakefile}
    1.35 -  (with crude source dependencies by default).  This file is located
    1.36 -  one level up from the @{verbatim Foo} directory location.  Now
    1.37 -  invoke
    1.38 -\begin{ttbox}
    1.39 -  isabelle make Foo
    1.40 -\end{ttbox}
    1.41 -  to run the @{verbatim Foo} session, with browser information and
    1.42 -  document preparation enabled.  Unless any errors are reported by
    1.43 -  Isabelle or {\LaTeX}, the output will appear inside the directory
    1.44 -  defined by the @{verbatim ISABELLE_BROWSER_INFO} setting (as
    1.45 -  reported by the batch job in verbose mode).
    1.46 -
    1.47 -  \medskip You may also consider to tune the @{verbatim usedir}
    1.48 -  options in @{verbatim IsaMakefile}, for example to switch the output
    1.49 -  format between @{verbatim pdf} and @{verbatim dvi}, or activate the
    1.50 -  @{verbatim "-D"} option to retain a second copy of the generated
    1.51 -  {\LaTeX} sources (for manual inspection or separate runs of
    1.52 -  @{executable latex}).
    1.53 -
    1.54 -  \medskip See \emph{The Isabelle System Manual} \cite{isabelle-sys}
    1.55 -  for further details on Isabelle logic sessions and theory
    1.56 -  presentation.  The Isabelle/HOL tutorial \cite{isabelle-hol-book}
    1.57 -  also covers theory presentation to some extent.
    1.58 -*}
    1.59 +  The Isabelle/HOL tutorial \cite{isabelle-hol-book} also covers
    1.60 +  theory presentation to some extent.  *}
    1.61  
    1.62  
    1.63  section {* Markup commands \label{sec:markup} *}
    1.64 @@ -418,9 +384,8 @@
    1.65  
    1.66    For boolean flags, ``@{text "name = true"}'' may be abbreviated as
    1.67    ``@{text name}''.  All of the above flags are disabled by default,
    1.68 -  unless changed from ML, say in the @{verbatim "ROOT.ML"} of the
    1.69 -  logic session.
    1.70 -*}
    1.71 +  unless changed specifically for a logic session in the corresponding
    1.72 +  @{verbatim "ROOT"} file.  *}
    1.73  
    1.74  
    1.75  section {* Markup via command tags \label{sec:tags} *}

     2.1 --- a/src/Doc/System/Basics.thy	Sat Jan 26 13:49:48 2013 +0100
     2.2 +++ b/src/Doc/System/Basics.thy	Sat Jan 26 16:10:50 2013 +0100
     2.3 @@ -495,10 +495,6 @@
     2.4  isabelle-process -r Test
     2.5  \end{ttbox}
     2.6  
     2.7 -  \medskip Note that manual session management like this does
     2.8 -  \emph{not} provide proper setup for theory presentation.  This would
     2.9 -  require @{tool usedir}.
    2.10 -
    2.11    \bigskip The next example demonstrates batch execution of Isabelle.
    2.12    We retrieve the @{verbatim Main} theory value from the theory loader
    2.13    within ML (observe the delicate quoting rules for the Bash shell

     3.1 --- a/src/Doc/Tutorial/Documents/Documents.thy	Sat Jan 26 13:49:48 2013 +0100
     3.2 +++ b/src/Doc/Tutorial/Documents/Documents.thy	Sat Jan 26 16:10:50 2013 +0100
     3.3 @@ -347,18 +347,21 @@
     3.4    (usually rooted at \verb,~/.isabelle/IsabelleXXXX/browser_info,).
     3.5  
     3.6    \medskip The easiest way to manage Isabelle sessions is via
     3.7 -  \texttt{isabelle mkdir} (generates an initial session source setup)
     3.8 -  and \texttt{isabelle make} (run sessions controlled by
     3.9 -  \texttt{IsaMakefile}).  For example, a new session
    3.10 -  \texttt{MySession} derived from \texttt{HOL} may be produced as
    3.11 -  follows:
    3.12 +  \texttt{isabelle mkroot} (to generate an initial session source
    3.13 +  setup) and \texttt{isabelle build} (to run sessions as specified in
    3.14 +  the corresponding \texttt{ROOT} file).  These Isabelle tools are
    3.15 +  described in further detail in the \emph{Isabelle System Manual}
    3.16 +  \cite{isabelle-sys}.
    3.17 +
    3.18 +  For example, a new session \texttt{MySession} (with document
    3.19 +  preparation) may be produced as follows:
    3.20  
    3.21  \begin{verbatim}
    3.22 -  isabelle mkdir HOL MySession
    3.23 -  isabelle make
    3.24 +  isabelle mkroot -d MySession
    3.25 +  isabelle build -D MySession
    3.26  \end{verbatim}
    3.27  
    3.28 -  The \texttt{isabelle make} job also informs about the file-system
    3.29 +  The \texttt{isabelle build} job also informs about the file-system
    3.30    location of the ultimate results.  The above dry run should be able
    3.31    to produce some \texttt{document.pdf} (with dummy title, empty table
    3.32    of contents etc.).  Any failure at this stage usually indicates
    3.33 @@ -372,10 +375,9 @@
    3.34    \item Directory \texttt{MySession} holds the required theory files
    3.35    $T@1$\texttt{.thy}, \dots, $T@n$\texttt{.thy}.
    3.36  
    3.37 -  \item File \texttt{MySession/ROOT.ML} holds appropriate ML commands
    3.38 -  for loading all wanted theories, usually just
    3.39 -  ``\texttt{use_thy"$T@i$";}'' for any $T@i$ in leaf position of the
    3.40 -  dependency graph.
    3.41 +  \item File \texttt{MySession/ROOT} specifies the session options and
    3.42 +  content, with declarations for all wanted theories; it is sufficient
    3.43 +  to specify the terminal nodes of the theory dependency graph.
    3.44  
    3.45    \item Directory \texttt{MySession/document} contains everything
    3.46    required for the {\LaTeX} stage; only \texttt{root.tex} needs to be
    3.47 @@ -389,17 +391,10 @@
    3.48    \verb,\input{session}, in the body of \texttt{root.tex} does the job
    3.49    in most situations.
    3.50  
    3.51 -  \item \texttt{IsaMakefile} holds appropriate dependencies and
    3.52 -  invocations of Isabelle tools to control the batch job.  In fact,
    3.53 -  several sessions may be managed by the same \texttt{IsaMakefile}.
    3.54 -  See the \emph{Isabelle System Manual} \cite{isabelle-sys} 
    3.55 -  for further details, especially on
    3.56 -  \texttt{isabelle usedir} and \texttt{isabelle make}.
    3.57 -
    3.58    \end{itemize}
    3.59  
    3.60 -  One may now start to populate the directory \texttt{MySession}, and
    3.61 -  the file \texttt{MySession/ROOT.ML} accordingly.  The file
    3.62 +  One may now start to populate the directory \texttt{MySession} and
    3.63 +  its \texttt{ROOT} file accordingly.  The file
    3.64    \texttt{MySession/document/root.tex} should also be adapted at some
    3.65    point; the default version is mostly self-explanatory.  Note that
    3.66    \verb,\isabellestyle, enables fine-tuning of the general appearance
    3.67 @@ -719,14 +714,18 @@
    3.68    collection of theories changes.
    3.69  
    3.70    Alternatively, one may tune the theory loading process in
    3.71 -  \texttt{ROOT.ML} itself: traversal of the theory dependency graph
    3.72 -  may be fine-tuned by adding \verb,use_thy, invocations, although
    3.73 -  topological sorting still has to be observed.  Moreover, the ML
    3.74 -  operator \verb,no_document, temporarily disables document generation
    3.75 -  while executing a theory loader command.  Its usage is like this:
    3.76 +  \texttt{ROOT} itself: some sequential order of \textbf{theories}
    3.77 +  sections may enforce a certain traversal of the dependency graph,
    3.78 +  although this could degrade parallel processing.  The nodes of each
    3.79 +  sub-graph that is specified here are presented in some topological
    3.80 +  order of their formal dependencies.
    3.81 +
    3.82 +  Moreover, the system build option \verb,document=false, allows to
    3.83 +  disable document generation for some theories.  Its usage in the
    3.84 +  session \texttt{ROOT} is like this:
    3.85  
    3.86  \begin{verbatim}
    3.87 -  no_document use_thy "T";
    3.88 +  theories [document = false] T
    3.89  \end{verbatim}
    3.90  
    3.91    \medskip Theory output may be suppressed more selectively, either
    3.92 @@ -753,7 +752,7 @@
    3.93    tagged region, in order to keep, drop, or fold the corresponding
    3.94    parts of the document.  See the \emph{Isabelle System Manual}
    3.95    \cite{isabelle-sys} for further details, especially on
    3.96 -  \texttt{isabelle usedir} and \texttt{isabelle document}.
    3.97 +  \texttt{isabelle build} and \texttt{isabelle document}.
    3.98  
    3.99    Ignored material is specified by delimiting the original formal
   3.100    source with special source comments