# HG changeset patch # User wenzelm # Date 1359213050 -3600 # Node ID a22b134f862e794a1f6b975f31fcfd899151f10e # Parent fbcc2d31463526c586b2a1ca11d7ddea2fb5da80 updated explanations of document preparation; diff -r fbcc2d314635 -r a22b134f862e src/Doc/IsarRef/Document_Preparation.thy --- 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} *} diff -r fbcc2d314635 -r a22b134f862e src/Doc/System/Basics.thy --- 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 diff -r fbcc2d314635 -r a22b134f862e src/Doc/Tutorial/Documents/Documents.thy --- 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