1.1 --- a/doc-src/TutorialI/Documents/document/Documents.tex Wed Jan 09 14:44:18 2002 +0100
1.2 +++ b/doc-src/TutorialI/Documents/document/Documents.tex Wed Jan 09 14:44:24 2002 +0100
1.3 @@ -337,15 +337,15 @@
1.4 In contrast to the highly interactive mode of Isabelle/Isar theory
1.5 development, the document preparation stage essentially works in
1.6 batch-mode. An Isabelle \bfindex{session} consists of a collection
1.7 - of theory source files that contribute to an output document
1.8 + of theory source files that may contribute to an output document
1.9 eventually. Each session is derived from a single parent, usually
1.10 an object-logic image like \texttt{HOL}. This results in an overall
1.11 tree structure, which is reflected by the output location in the
1.12 file system (usually rooted at \verb,~/isabelle/browser_info,).
1.13
1.14 \medskip The easiest way to manage Isabelle sessions is via
1.15 - \texttt{isatool mkdir} (generates an initial source setup) and
1.16 - \texttt{isatool make} (runs a session controlled by
1.17 + \texttt{isatool mkdir} (generates an initial session source setup)
1.18 + and \texttt{isatool make} (run sessions controlled by
1.19 \texttt{IsaMakefile}). For example, a new session
1.20 \texttt{MySession} derived from \texttt{HOL} may be produced as
1.21 follows:
1.22 @@ -355,15 +355,14 @@
1.23 isatool make
1.24 \end{verbatim}
1.25
1.26 - The \texttt{isatool make} job tells about the file-system location
1.27 - of the ultimate results. The above dry run should be able to
1.28 - produce some \texttt{document.pdf} of a single page (with dummy
1.29 - title, empty table of contents etc.). Any failure at that stage
1.30 - usually indicates technical problems of the {\LaTeX}
1.31 - installation.\footnote{Especially make sure that \texttt{pdflatex}
1.32 - is present; if all fails one may fall back on DVI output by changing
1.33 - \texttt{usedir} options in \texttt{IsaMakefile}
1.34 - \cite{isabelle-sys}.}
1.35 + The \texttt{isatool make} job also informs about the file-system
1.36 + location of the ultimate results. The above dry run should be able
1.37 + to produce some \texttt{document.pdf} (with dummy title, empty table
1.38 + of contents etc.). Any failure at that stage usually indicates
1.39 + technical problems of the {\LaTeX} installation.\footnote{Especially
1.40 + make sure that \texttt{pdflatex} is present; if all fails one may
1.41 + fall back on DVI output by changing \texttt{usedir} options in
1.42 + \texttt{IsaMakefile} \cite{isabelle-sys}.}
1.43
1.44 \medskip The detailed arrangement of the session sources is as
1.45 follows:
1.46 @@ -398,37 +397,32 @@
1.47
1.48 \end{itemize}
1.49
1.50 - With everything put in its proper place, \texttt{isatool make}
1.51 - should be sufficient to process the Isabelle session completely,
1.52 - with the generated document appearing in its proper place.
1.53 + One may now start to populate the directory \texttt{MySession}, and
1.54 + the file \texttt{MySession/ROOT.ML} accordingly.
1.55 + \texttt{MySession/document/root.tex} should also be adapted at some
1.56 + point; the default version is mostly self-explanatory. Note that
1.57 + \verb,\isabellestyle, enables fine-tuning of the general appearance
1.58 + of characters and mathematical symbols (see also
1.59 + \S\ref{sec:doc-prep-symbols}).
1.60
1.61 - \medskip One may now start to populate the directory
1.62 - \texttt{MySession}, and the file \texttt{MySession/ROOT.ML}
1.63 - accordingly. \texttt{MySession/document/root.tex} should also be
1.64 - adapted at some point; the default version is mostly
1.65 - self-explanatory. Note that \verb,\isabellestyle, enables
1.66 - fine-tuning of the general appearance of characters and mathematical
1.67 - symbols (see also \S\ref{sec:doc-prep-symbols}).
1.68 + Especially observe the included {\LaTeX} packages \texttt{isabelle}
1.69 + (mandatory), \texttt{isabellesym} (required for mathematical
1.70 + symbols), and the final \texttt{pdfsetup} (provides handsome
1.71 + defaults for \texttt{hyperref}, including URL markup) --- all three
1.72 + are distributed with Isabelle. Further packages may be required in
1.73 + particular applications, e.g.\ for unusual mathematical symbols.
1.74
1.75 - Especially observe inclusion of the {\LaTeX} packages
1.76 - \texttt{isabelle} (mandatory), and \texttt{isabellesym} (required
1.77 - for mathematical symbols), and the final \texttt{pdfsetup} (provides
1.78 - handsome defaults for \texttt{hyperref}, including URL markup).
1.79 - Further packages may be required in particular applications, e.g.\
1.80 - for unusual Isabelle symbols.
1.81 -
1.82 - \medskip Additional files for the {\LaTeX} stage may be included in
1.83 - the directory \texttt{MySession/document}, too, such as {\TeX}
1.84 - sources or graphics). In particular, adding \texttt{root.bib} here
1.85 - (with that specific name) causes an automatic run of \texttt{bibtex}
1.86 - to process a bibliographic database; see also \texttt{isatool
1.87 - document} covered in \cite{isabelle-sys}.
1.88 + \medskip Additional files for the {\LaTeX} stage may be put into the
1.89 + \texttt{MySession/document} directory, too. In particular, adding
1.90 + \texttt{root.bib} here (with that specific name) causes an automatic
1.91 + run of \texttt{bibtex} to process a bibliographic database; see also
1.92 + \texttt{isatool document} covered in \cite{isabelle-sys}.
1.93
1.94 \medskip Any failure of the document preparation phase in an
1.95 Isabelle batch session leaves the generated sources in their target
1.96 location (as pointed out by the accompanied error message). This
1.97 - enables users to trace {\LaTeX} at the file positions of the
1.98 - generated material.%
1.99 + enables users to trace {\LaTeX} problems with the target files at
1.100 + hand.%
1.101 \end{isamarkuptext}%
1.102 \isamarkuptrue%
1.103 %