--- a/doc-src/System/present.tex Tue Aug 16 13:42:19 2005 +0200
+++ b/doc-src/System/present.tex Tue Aug 16 13:42:20 2005 +0200
@@ -363,9 +363,11 @@
Options are:
-D PATH dump generated document sources into PATH
-P PATH set path for remote theory browsing information
+ -V VERSION declare alternative document VERSION
-b build mode (output heap image, using current dir)
-c BOOL tell ML system to compress output image (default true)
-d FORMAT build document as FORMAT (default false)
+ -f NAME use ML file NAME (default ROOT.ML)
-g BOOL generate session graph image for document (default false)
-i BOOL generate theory browser information (default false)
-m MODE add print mode for output
@@ -422,8 +424,17 @@
\texttt{document} directory. See \S\ref{sec:tool-document} and
\S\ref{sec:tool-latex} for more details.
-The \texttt{-g} option produces images of the theory dependency graph (cf.\
-\S\ref{sec:browse}) for inclusion in the generated document, both as
+\medskip The \texttt{-V} option (which may be repeated) declares alternative
+document versions, consisting of name/tags pairs (cf.\ options \texttt{-n} and
+\texttt{-t} of the \texttt{document} tool, \S\ref{sec:tool-document}). The
+standard document is equivalent to ``\texttt{document=theory,proof,ML}'',
+which means that all theory begin/end commands, proof body texts, and ML code
+will be presented faithfully. An alternative version
+``\texttt{outline=/proof/ML}'' would fold proof and ML parts, replacing the
+original text by a short place-holder.
+
+\medskip The \texttt{-g} option produces images of the theory dependency graph
+(cf.\ \S\ref{sec:browse}) for inclusion in the generated document, both as
\texttt{session_graph.eps} and \texttt{session_graph.pdf} at the same time.
To include this in the final {\LaTeX} document one could say
\verb,\includegraphics{session_graph}, in \texttt{document/root.tex} (omitting
@@ -476,8 +487,10 @@
Options are:
-c cleanup -- be aggressive in removing old stuff
+ -n NAME specify document name (default 'document')
-o FORMAT specify output format: dvi (default), dvi.gz, ps,
ps.gz, pdf
+ -t TAGS specify tagged region markup
Prepare the theory session document in DIR (default 'document')
producing the specified output format.
@@ -488,6 +501,24 @@
It may be manually invoked on the generated browser information document
output as well, e.g.\ in case of errors encountered in the batch run.
+\medskip The \texttt{-c} option tells the \texttt{document} tool to dispose
+the document sources after successful operation. This is the right thing to
+do for sources generated by an Isabelle process, but take care of your files
+in manual document preparation!
+
+\medskip The \texttt{-n} and \texttt{-o} option specify the final output file
+name and format, the default is ``\texttt{document.dvi}''. Note that the
+result will appear in the parent of the target \texttt{DIR}.
+
+\medskip The \texttt{-t} option tells {\LaTeX} how to interpret tagged
+Isabelle command regions. Tags are specified as a comma separated list of
+modifier/name pairs: ``\verb,+,$foo$'' (or just ``$foo$'') means to keep,
+``\verb,-,$foo$'' to drop, and ``\verb,/,$foo$'' to fold text tagged as $foo$.
+The builtin default is equivalent to the tag specification
+``\texttt{/theory,/proof,/ML,+visible,-invisible}''; see also the {\LaTeX}
+macros \verb,\isakeeptag,, \verb,\isadroptag,, and \verb,\isafoldtag, in
+\texttt{isabelle.sty}.
+
\medskip Document preparation requires a properly setup ``\texttt{document}''
directory within the logic session sources. This directory is supposed to
contain all the files needed to produce the final document --- apart from the