--- a/src/Doc/System/Presentation.thy Mon Dec 11 17:52:05 2017 +0100
+++ b/src/Doc/System/Presentation.thy Mon Dec 11 18:39:24 2017 +0100
@@ -151,7 +151,6 @@
\<open>Usage: isabelle document [OPTIONS]
Options are:
- -c aggressive cleanup of -d DIR content
-d DIR document output directory (default "output/document")
-n NAME document name (default "document")
-o FORMAT document format: pdf (default), dvi
@@ -168,12 +167,6 @@
run.
\<^medskip>
- The \<^verbatim>\<open>-c\<close> option tells @{tool document} 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>
Option \<^verbatim>\<open>-d\<close> specifies an laternative document output directory. The default
is \<^verbatim>\<open>output/document\<close> (derived from the document name). Note that the result
will appear in the parent of this directory.
@@ -240,10 +233,10 @@
we recommend to include \<^file>\<open>~~/lib/texinputs/pdfsetup.sty\<close> as well.
\<^medskip>
- As a final step of Isabelle document preparation, @{tool document}~\<^verbatim>\<open>-c\<close> is
- run on the resulting copy of the \<^verbatim>\<open>document\<close> directory. Thus the actual
- output document is built and installed in its proper place. The generated
- sources are deleted after successful run of {\LaTeX} and friends.
+ As a final step of Isabelle document preparation, @{tool document} is run on
+ the generated \<^verbatim>\<open>output/document\<close> directory. Thus the actual output document
+ is built and installed in its proper place. The generated sources are
+ deleted after successful run of {\LaTeX} and friends.
Some care is needed if the document output location is configured
differently, say within a directory whose content is still required