--- a/doc-src/System/present.tex Wed Aug 31 15:46:31 2005 +0200
+++ b/doc-src/System/present.tex Wed Aug 31 15:46:32 2005 +0200
@@ -361,6 +361,7 @@
Usage: usedir [OPTIONS] LOGIC NAME
Options are:
+ -C BOOL copy existing document directory to -D PATH (default true)
-D PATH dump generated document sources into PATH
-P PATH set path for remote theory browsing information
-V VERSION declare alternative document VERSION
@@ -443,15 +444,16 @@
the file-name extension enables {\LaTeX} to select to correct version, either
for the DVI or PDF output path).
-\medskip The \texttt{-D} option causes the generated document sources
-(including the user's template of \texttt{document/root.tex} etc.) to be
+\medskip The \texttt{-D} option causes the generated document sources to be
dumped at location \texttt{PATH}; this path is relative to the session's main
-directory. For example, \texttt{isatool usedir -D generated HOL Foo} will
-produces a complete set of document sources at \texttt{Foo/generated}.
-Subsequent invocation of \texttt{isatool document Foo/generated} (see also
-\S\ref{sec:tool-document}) will process the final result independently of an
-Isabelle job. This decoupled mode of operation facilitates debugging of
-serious {\LaTeX} errors, for example.
+directory. If the \texttt{-C} option is true, this will include a copy of an
+existing \texttt{document} directory as provided by the user. For example,
+\texttt{isatool usedir -D generated HOL Foo} produces a complete set of
+document sources at \texttt{Foo/generated}. Subsequent invocation of
+\texttt{isatool document Foo/generated} (see also \S\ref{sec:tool-document})
+will process the final result independently of an Isabelle job. This
+decoupled mode of operation facilitates debugging of serious {\LaTeX} errors,
+for example.
\medskip The \texttt{-p} option determines the level of detail for internal
proof objects, see also the \emph{Isabelle Reference