# HG changeset patch
# User wenzelm
# Date 1124192540 -7200
# Node ID a7da4123523e460569d95bde4c977af7e13755d1
# Parent  80fceeb2bcef855b7c18f672b04f07d7379eed50
isatool usedir: option -V and -f;
isatool document: option -n and -t;

diff -r 80fceeb2bcef -r a7da4123523e doc-src/System/present.tex
--- 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