--- a/src/Doc/IsarRef/Document_Preparation.thy Sat Jan 26 13:49:48 2013 +0100
+++ b/src/Doc/IsarRef/Document_Preparation.thy Sat Jan 26 16:10:50 2013 +0100
@@ -5,51 +5,17 @@
chapter {* Document preparation \label{ch:document-prep} *}
text {* Isabelle/Isar provides a simple document preparation system
- based on regular {PDF-\LaTeX} technology, with full support for
- hyper-links and bookmarks. Thus the results are well suited for WWW
- browsing and as printed copies.
-
- \medskip Isabelle generates {\LaTeX} output while running a
- \emph{logic session} (see also \cite{isabelle-sys}). Getting
- started with a working configuration for common situations is quite
- easy by using the Isabelle @{verbatim mkdir} and @{verbatim make}
- tools. First invoke
-\begin{ttbox}
- isabelle mkdir Foo
-\end{ttbox}
- to initialize a separate directory for session @{verbatim Foo} (it
- is safe to experiment, since @{verbatim "isabelle mkdir"} never
- overwrites existing files). Ensure that @{verbatim "Foo/ROOT.ML"}
- holds ML commands to load all theories required for this session;
- furthermore @{verbatim "Foo/document/root.tex"} should include any
- special {\LaTeX} macro packages required for your document (the
- default is usually sufficient as a start).
+ based on regular {PDF-\LaTeX} technology, with support for
+ hyper-links and bookmarks within that format. Thus the results are
+ well suited for WWW browsing and as printed copies.
- The session is controlled by a separate @{verbatim IsaMakefile}
- (with crude source dependencies by default). This file is located
- one level up from the @{verbatim Foo} directory location. Now
- invoke
-\begin{ttbox}
- isabelle make Foo
-\end{ttbox}
- to run the @{verbatim Foo} session, with browser information and
- document preparation enabled. Unless any errors are reported by
- Isabelle or {\LaTeX}, the output will appear inside the directory
- defined by the @{verbatim ISABELLE_BROWSER_INFO} setting (as
- reported by the batch job in verbose mode).
+ {\LaTeX} output is generated while processing a \emph{session} in
+ batch mode, as explained in the \emph{The Isabelle System Manual}
+ \cite{isabelle-sys}. The main Isabelle tools to get started with
+ document prepation are @{tool_ref mkroot} and @{tool_ref build}.
- \medskip You may also consider to tune the @{verbatim usedir}
- options in @{verbatim IsaMakefile}, for example to switch the output
- format between @{verbatim pdf} and @{verbatim dvi}, or activate the
- @{verbatim "-D"} option to retain a second copy of the generated
- {\LaTeX} sources (for manual inspection or separate runs of
- @{executable latex}).
-
- \medskip See \emph{The Isabelle System Manual} \cite{isabelle-sys}
- for further details on Isabelle logic sessions and theory
- presentation. The Isabelle/HOL tutorial \cite{isabelle-hol-book}
- also covers theory presentation to some extent.
-*}
+ The Isabelle/HOL tutorial \cite{isabelle-hol-book} also covers
+ theory presentation to some extent. *}
section {* Markup commands \label{sec:markup} *}
@@ -418,9 +384,8 @@
For boolean flags, ``@{text "name = true"}'' may be abbreviated as
``@{text name}''. All of the above flags are disabled by default,
- unless changed from ML, say in the @{verbatim "ROOT.ML"} of the
- logic session.
-*}
+ unless changed specifically for a logic session in the corresponding
+ @{verbatim "ROOT"} file. *}
section {* Markup via command tags \label{sec:tags} *}
--- a/src/Doc/System/Basics.thy Sat Jan 26 13:49:48 2013 +0100
+++ b/src/Doc/System/Basics.thy Sat Jan 26 16:10:50 2013 +0100
@@ -495,10 +495,6 @@
isabelle-process -r Test
\end{ttbox}
- \medskip Note that manual session management like this does
- \emph{not} provide proper setup for theory presentation. This would
- require @{tool usedir}.
-
\bigskip The next example demonstrates batch execution of Isabelle.
We retrieve the @{verbatim Main} theory value from the theory loader
within ML (observe the delicate quoting rules for the Bash shell
--- a/src/Doc/Tutorial/Documents/Documents.thy Sat Jan 26 13:49:48 2013 +0100
+++ b/src/Doc/Tutorial/Documents/Documents.thy Sat Jan 26 16:10:50 2013 +0100
@@ -347,18 +347,21 @@
(usually rooted at \verb,~/.isabelle/IsabelleXXXX/browser_info,).
\medskip The easiest way to manage Isabelle sessions is via
- \texttt{isabelle mkdir} (generates an initial session source setup)
- and \texttt{isabelle make} (run sessions controlled by
- \texttt{IsaMakefile}). For example, a new session
- \texttt{MySession} derived from \texttt{HOL} may be produced as
- follows:
+ \texttt{isabelle mkroot} (to generate an initial session source
+ setup) and \texttt{isabelle build} (to run sessions as specified in
+ the corresponding \texttt{ROOT} file). These Isabelle tools are
+ described in further detail in the \emph{Isabelle System Manual}
+ \cite{isabelle-sys}.
+
+ For example, a new session \texttt{MySession} (with document
+ preparation) may be produced as follows:
\begin{verbatim}
- isabelle mkdir HOL MySession
- isabelle make
+ isabelle mkroot -d MySession
+ isabelle build -D MySession
\end{verbatim}
- The \texttt{isabelle make} job also informs about the file-system
+ The \texttt{isabelle build} job also informs about the file-system
location of the ultimate results. The above dry run should be able
to produce some \texttt{document.pdf} (with dummy title, empty table
of contents etc.). Any failure at this stage usually indicates
@@ -372,10 +375,9 @@
\item Directory \texttt{MySession} holds the required theory files
$T@1$\texttt{.thy}, \dots, $T@n$\texttt{.thy}.
- \item File \texttt{MySession/ROOT.ML} holds appropriate ML commands
- for loading all wanted theories, usually just
- ``\texttt{use_thy"$T@i$";}'' for any $T@i$ in leaf position of the
- dependency graph.
+ \item File \texttt{MySession/ROOT} specifies the session options and
+ content, with declarations for all wanted theories; it is sufficient
+ to specify the terminal nodes of the theory dependency graph.
\item Directory \texttt{MySession/document} contains everything
required for the {\LaTeX} stage; only \texttt{root.tex} needs to be
@@ -389,17 +391,10 @@
\verb,\input{session}, in the body of \texttt{root.tex} does the job
in most situations.
- \item \texttt{IsaMakefile} holds appropriate dependencies and
- invocations of Isabelle tools to control the batch job. In fact,
- several sessions may be managed by the same \texttt{IsaMakefile}.
- See the \emph{Isabelle System Manual} \cite{isabelle-sys}
- for further details, especially on
- \texttt{isabelle usedir} and \texttt{isabelle make}.
-
\end{itemize}
- One may now start to populate the directory \texttt{MySession}, and
- the file \texttt{MySession/ROOT.ML} accordingly. The file
+ One may now start to populate the directory \texttt{MySession} and
+ its \texttt{ROOT} file accordingly. The file
\texttt{MySession/document/root.tex} should also be adapted at some
point; the default version is mostly self-explanatory. Note that
\verb,\isabellestyle, enables fine-tuning of the general appearance
@@ -719,14 +714,18 @@
collection of theories changes.
Alternatively, one may tune the theory loading process in
- \texttt{ROOT.ML} itself: traversal of the theory dependency graph
- may be fine-tuned by adding \verb,use_thy, invocations, although
- topological sorting still has to be observed. Moreover, the ML
- operator \verb,no_document, temporarily disables document generation
- while executing a theory loader command. Its usage is like this:
+ \texttt{ROOT} itself: some sequential order of \textbf{theories}
+ sections may enforce a certain traversal of the dependency graph,
+ although this could degrade parallel processing. The nodes of each
+ sub-graph that is specified here are presented in some topological
+ order of their formal dependencies.
+
+ Moreover, the system build option \verb,document=false, allows to
+ disable document generation for some theories. Its usage in the
+ session \texttt{ROOT} is like this:
\begin{verbatim}
- no_document use_thy "T";
+ theories [document = false] T
\end{verbatim}
\medskip Theory output may be suppressed more selectively, either
@@ -753,7 +752,7 @@
tagged region, in order to keep, drop, or fold the corresponding
parts of the document. See the \emph{Isabelle System Manual}
\cite{isabelle-sys} for further details, especially on
- \texttt{isabelle usedir} and \texttt{isabelle document}.
+ \texttt{isabelle build} and \texttt{isabelle document}.
Ignored material is specified by delimiting the original formal
source with special source comments