updated documentation;
authorwenzelm
Mon Dec 11 18:39:24 2017 +0100 (17 months ago)
changeset 67185d5e51ba21561
parent 67184 ecc786cb3b7b
child 67186 a58bbe66ac81
updated documentation;
src/Doc/System/Presentation.thy
     1.1 --- a/src/Doc/System/Presentation.thy	Mon Dec 11 17:52:05 2017 +0100
     1.2 +++ b/src/Doc/System/Presentation.thy	Mon Dec 11 18:39:24 2017 +0100
     1.3 @@ -151,7 +151,6 @@
     1.4  \<open>Usage: isabelle document [OPTIONS]
     1.5  
     1.6    Options are:
     1.7 -    -c           aggressive cleanup of -d DIR content
     1.8      -d DIR       document output directory (default "output/document")
     1.9      -n NAME      document name (default "document")
    1.10      -o FORMAT    document format: pdf (default), dvi
    1.11 @@ -168,12 +167,6 @@
    1.12    run.
    1.13  
    1.14    \<^medskip>
    1.15 -  The \<^verbatim>\<open>-c\<close> option tells @{tool document} to dispose the document sources
    1.16 -  after successful operation! This is the right thing to do for sources
    1.17 -  generated by an Isabelle process, but take care of your files in manual
    1.18 -  document preparation!
    1.19 -
    1.20 -  \<^medskip>
    1.21    Option \<^verbatim>\<open>-d\<close> specifies an laternative document output directory. The default
    1.22    is \<^verbatim>\<open>output/document\<close> (derived from the document name). Note that the result
    1.23    will appear in the parent of this directory.
    1.24 @@ -240,10 +233,10 @@
    1.25    we recommend to include \<^file>\<open>~~/lib/texinputs/pdfsetup.sty\<close> as well.
    1.26  
    1.27    \<^medskip>
    1.28 -  As a final step of Isabelle document preparation, @{tool document}~\<^verbatim>\<open>-c\<close> is
    1.29 -  run on the resulting copy of the \<^verbatim>\<open>document\<close> directory. Thus the actual
    1.30 -  output document is built and installed in its proper place. The generated
    1.31 -  sources are deleted after successful run of {\LaTeX} and friends.
    1.32 +  As a final step of Isabelle document preparation, @{tool document} is run on
    1.33 +  the generated \<^verbatim>\<open>output/document\<close> directory. Thus the actual output document
    1.34 +  is built and installed in its proper place. The generated sources are
    1.35 +  deleted after successful run of {\LaTeX} and friends.
    1.36  
    1.37    Some care is needed if the document output location is configured
    1.38    differently, say within a directory whose content is still required