--- a/src/Doc/System/Presentation.thy Wed Nov 11 20:58:36 2020 +0100
+++ b/src/Doc/System/Presentation.thy Wed Nov 11 21:00:14 2020 +0100
@@ -15,37 +15,15 @@
HOL, and HOL from Pure), and application sessions further on in the
hierarchy.
- The tools @{tool_ref mkroot} and @{tool_ref build} provide the primary means
- for managing Isabelle sessions, including proper setup for presentation;
- @{tool build} tells the Isabelle process to run any additional stages
- required for document preparation, notably the @{tool_ref document} and
- @{tool_ref latex}. The complete tool chain for managing batch-mode Isabelle
- sessions is illustrated in \figref{fig:session-tools}.
-
- \begin{figure}[htbp]
- \begin{center}
- \begin{tabular}{lp{0.6\textwidth}}
-
- @{tool_ref mkroot} & invoked once by the user to initialize the
- session \<^verbatim>\<open>ROOT\<close> with optional \<^verbatim>\<open>document\<close>
- directory; \\
+ The command-line tools @{tool_ref mkroot} and @{tool_ref build} provide the
+ primary means for managing Isabelle sessions, including options for
+ presentation: ``\<^verbatim>\<open>document=pdf\<close>'' generates PDF output from the theory
+ session, and ``\<^verbatim>\<open>document_output=dir\<close>'' emits a copy of the document sources
+ with the PDF into the given directory (relative to the session directory).
- @{tool_ref build} & invoked repeatedly by the user to keep
- session output up-to-date (HTML, documents etc.); \\
-
- @{tool_ref process} & run through @{tool_ref build}; \\
-
- @{tool_ref document} & run by the Isabelle process if document
- preparation is enabled; \\
-
- @{tool_ref latex} & universal {\LaTeX} tool wrapper invoked
- multiple times by @{tool_ref document}; also useful for manual
- experiments; \\
-
- \end{tabular}
- \caption{The tool chain of Isabelle session presentation} \label{fig:session-tools}
- \end{center}
- \end{figure}
+ Alternatively, @{tool_ref document} may be used to turn the generated
+ {\LaTeX} sources of a session (exports from its build database) into PDF,
+ using suitable invocations of @{tool_ref latex}.
\<close>
@@ -145,101 +123,56 @@
section \<open>Preparing Isabelle session documents \label{sec:tool-document}\<close>
text \<open>
- The @{tool_def document} tool prepares logic session documents, processing
- the sources as provided by the user and generated by Isabelle. Its usage is:
+ The @{tool_def document} tool prepares logic session documents. Its usage
+ is:
@{verbatim [display]
-\<open>Usage: isabelle document [OPTIONS]
+\<open>Usage: isabelle document [OPTIONS] SESSION
Options are:
- -d DIR document output directory (default "output/document")
- -n NAME document name (default "document")
- -t TAGS markup for tagged regions
-
- Prepare the theory session document in document directory, producing the
- specified output format.
-\<close>}
+ -O set option "document_output", relative to current directory
+ -V verbose latex
+ -d DIR include session directory
+ -n no build of session
+ -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
+ -v verbose build
- This tool is usually run automatically as part of the Isabelle build
- process, provided document preparation has been enabled via suitable
- options. 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>
- Option \<^verbatim>\<open>-d\<close> specifies an alternative 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.
+ Prepare the theory document of a session.\<close>}
- \<^medskip>
- Option \<^verbatim>\<open>-n\<close> specifies the resulting document file name, the default is
- ``\<^verbatim>\<open>document\<close>'' (leading to ``\<^verbatim>\<open>document.pdf\<close>'').
+ Generated {\LaTeX} sources are taken from the session build database:
+ @{tool_ref build} is invoked beforehand to ensure that it is up-to-date, but
+ option \<^verbatim>\<open>-n\<close> suppresses that. Further files are generated on the spot,
+ notably essential Isabelle style files, and \<^verbatim>\<open>session.tex\<close> to input all
+ theory sources from the session (excluding imports from other sessions).
- \<^medskip>
- The \<^verbatim>\<open>-t\<close> option tells {\LaTeX} how to interpret tagged Isabelle command
- regions. Tags are specified as a comma separated list of modifier/name
- pairs: ``\<^verbatim>\<open>+\<close>\<open>foo\<close>'' (or just ``\<open>foo\<close>'') means to keep, ``\<^verbatim>\<open>-\<close>\<open>foo\<close>'' to
- drop, and ``\<^verbatim>\<open>/\<close>\<open>foo\<close>'' to fold text tagged as \<open>foo\<close>. The builtin default is
- equivalent to the tag specification
- ``\<^verbatim>\<open>+document,+theory,+proof,+ML,+visible,-invisible,+important,+unimportant\<close>'';
- see also the {\LaTeX} macros \<^verbatim>\<open>\isakeeptag\<close>, \<^verbatim>\<open>\isadroptag\<close>, and
- \<^verbatim>\<open>\isafoldtag\<close>, in \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close>.
+ \<^medskip> Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-o\<close>, \<^verbatim>\<open>-v\<close> have the same meaning as for @{tool build}.
- \<^medskip>
- Document preparation requires a \<^verbatim>\<open>document\<close> directory within the session
- sources. This directory is supposed to contain all the files needed to
- produce the final document --- apart from the actual theories which are
- generated by Isabelle.
+ \<^medskip> Option \<^verbatim>\<open>-V\<close> prints full output of {\LaTeX} tools.
- \<^medskip>
- For most practical purposes, @{tool document} is smart enough to create any
- of the specified output formats, taking \<^verbatim>\<open>root.tex\<close> supplied by the user as
- a starting point. This even includes multiple runs of {\LaTeX} to
- accommodate references and bibliographies (the latter assumes \<^verbatim>\<open>root.bib\<close>
- within the same directory).
+ \<^medskip> Option \<^verbatim>\<open>-O\<close>~\<open>dir\<close> specifies the @{system_option document_output} option
+ relative to the current directory, while \<^verbatim>\<open>-o document_output=\<close>\<open>dir\<close> is
+ relative to the session directory.
- In more complex situations, a separate \<^verbatim>\<open>build\<close> script for the document
- sources may be given. It is invoked with command-line arguments for the
- document format and the document variant name. The script needs to produce
- corresponding output files, e.g.\ \<^verbatim>\<open>root.pdf\<close> for target format \<^verbatim>\<open>pdf\<close> (and
- default variants). The main work can be again delegated to @{tool latex},
- but it is also possible to harvest generated {\LaTeX} sources and copy them
- elsewhere.
-
- \<^medskip>
- When running the session, Isabelle copies the content of the original
- \<^verbatim>\<open>document\<close> directory into its proper place within @{setting
- ISABELLE_BROWSER_INFO}, according to the session path and document variant.
- Then, for any processed theory \<open>A\<close> some {\LaTeX} source is generated and put
- there as \<open>A\<close>\<^verbatim>\<open>.tex\<close>. Furthermore, a list of all generated theory files is
- put into \<^verbatim>\<open>session.tex\<close>. Typically, the root {\LaTeX} file provided by the
- user would include \<^verbatim>\<open>session.tex\<close> to get a document containing all the
- theories.
+ For example, for output directory ``\<^verbatim>\<open>output\<close>'' and the default document
+ variant ``\<^verbatim>\<open>document\<close>'', the generated document sources are placed into the
+ subdirectory \<^verbatim>\<open>output/document/\<close> and the resulting PDF into
+ \<^verbatim>\<open>output/document.pdf\<close>.
- The {\LaTeX} versions of the theories require some macros defined in
- \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close>. Doing \<^verbatim>\<open>\usepackage{isabelle}\<close> in
- \<^verbatim>\<open>root.tex\<close> should be fine; the underlying @{tool latex} already includes an
- appropriate path specification for {\TeX} inputs.
-
- If the text contains any references to Isabelle symbols (such as \<^verbatim>\<open>\<forall>\<close>) then
- \<^verbatim>\<open>isabellesym.sty\<close> should be included as well. This package contains a
- standard set of {\LaTeX} macro definitions \<^verbatim>\<open>\isasym\<close>\<open>foo\<close> corresponding to
- \<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>foo\<close>\<^verbatim>\<open>>\<close>, see @{cite "isabelle-implementation"} for a complete list
- of predefined Isabelle symbols. Users may invent further symbols as well,
- just by providing {\LaTeX} macros in a similar fashion as in
- \<^file>\<open>~~/lib/texinputs/isabellesym.sty\<close> of the Isabelle distribution.
+ \<^medskip> Isabelle is usually smart enough to create the PDF from the given
+ \<^verbatim>\<open>root.tex\<close> and optional \<^verbatim>\<open>root.bib\<close> (bibliography) and \<^verbatim>\<open>root.idx\<close> (index)
+ using standard {\LaTeX} tools. Alternatively, \isakeyword{document\_files}
+ in the session \<^verbatim>\<open>ROOT\<close> may include an executable \<^verbatim>\<open>build\<close> script to take
+ care of that. It is invoked with command-line arguments for the document
+ format (\<^verbatim>\<open>pdf\<close>) and the document variant name. The script needs to produce
+ corresponding output files, e.g.\ \<^verbatim>\<open>root.pdf\<close> for default document variants
+ (the main work can be delegated to @{tool latex}). \<close>
- For proper setup of PDF documents (with hyperlinks and bookmarks),
- we recommend to include \<^file>\<open>~~/lib/texinputs/pdfsetup.sty\<close> as well.
+subsubsection \<open>Examples\<close>
- \<^medskip>
- 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.
+text \<open>
+ Produce the document from session \<^verbatim>\<open>FOL\<close> with full verbosity, and a copy in
+ the current directory (subdirectory \<^verbatim>\<open>document\<close> and file \<^verbatim>\<open>document.pdf)\<close>:
- Some care is needed if the document output location is configured
- differently, say within a directory whose content is still required
- afterwards!
+ @{verbatim [display] \<open>isabelle document -v -V -O. FOL\<close>}
\<close>