--- a/src/Doc/System/Presentation.thy Fri Dec 03 13:32:58 2021 +0100
+++ b/src/Doc/System/Presentation.thy Fri Dec 03 15:11:16 2021 +0100
@@ -161,17 +161,33 @@
\<^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. Actual command-lines are given by settings
- @{setting_ref ISABELLE_PDFLATEX}, @{setting_ref ISABELLE_LUALATEX},
+ @{setting_ref ISABELLE_LUALATEX} (or @{setting_ref ISABELLE_PDFLATEX}),
@{setting_ref ISABELLE_BIBTEX}, @{setting_ref ISABELLE_MAKEINDEX}: these
variables are used without quoting in shell scripts, and thus may contain
additional options.
- Alternatively, the session \<^verbatim>\<open>ROOT\<close> may include an option
- \<^verbatim>\<open>document_build=build\<close> together with an executable \<^verbatim>\<open>build\<close> script in
- \isakeyword{document\_files}: 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 system option @{system_option_def "document_build"} specifies an
+ alternative build engine, e.g. within the session \<^verbatim>\<open>ROOT\<close> file as
+ ``\<^verbatim>\<open>options [document_build = pdflatex]\<close>''. The following standard engines
+ are available:
+
+ \<^item> \<^verbatim>\<open>lualatex\<close> (default) uses the shell command \<^verbatim>\<open>$ISABELLE_LUALATEX\<close> on
+ the main \<^verbatim>\<open>root.tex\<close> file, with further runs of \<^verbatim>\<open>$ISABELLE_BIBTEX\<close> and
+ \<^verbatim>\<open>$ISABELLE_MAKEINDEX\<close> as required.
+
+ \<^item> \<^verbatim>\<open>pdflatex\<close> uses \<^verbatim>\<open>$ISABELLE_PDFLATEX\<close> instead of \<^verbatim>\<open>$ISABELLE_LUALATEX\<close>,
+ and the other tools as above.
+
+ \<^item> \<^verbatim>\<open>build\<close> invokes an executable script of the same name in a private
+ directory containing all \isakeyword{document\_files} and other generated
+ document sources. The script is invoked as ``\<^verbatim>\<open>./build pdf\<close>~\<open>name\<close>'' for
+ the document variant name; it needs to produce a corresponding
+ \<open>name\<close>\<^verbatim>\<open>.pdf\<close> file by arbitrary means on its own.
+
+ Further engines can be defined by add-on components in Isabelle/Scala
+ (\secref{sec:scala-build}), providing a service class derived from
+ \<^scala_type>\<open>isabelle.Document_Build.Engine\<close>. Available classes are listed
+ in \<^scala>\<open>isabelle.Document_Build.engines\<close>.
\<close>
--- a/src/Doc/System/Sessions.thy Fri Dec 03 13:32:58 2021 +0100
+++ b/src/Doc/System/Sessions.thy Fri Dec 03 15:11:16 2021 +0100
@@ -212,6 +212,9 @@
default configuration with output readily available to the author of the
document.
+ \<^item> @{system_option_def "document_echo"} informs about document file names
+ during session presentation.
+
\<^item> @{system_option_def "document_variants"} specifies document variants as
a colon-separated list of \<open>name=tags\<close> entries. The default name
\<^verbatim>\<open>document\<close>, without additional tags.
@@ -239,10 +242,21 @@
is occasionally useful to control the global visibility of commands via
session options (e.g.\ in \<^verbatim>\<open>ROOT\<close>).
+ \<^item> @{system_option_def "document_comment_latex"} enables regular {\LaTeX}
+ \<^verbatim>\<open>comment.sty\<close>, instead of the historic version for plain {\TeX}
+ (default). The latter is much faster, but in conflict with {\LaTeX}
+ classes like Dagstuhl
+ LIPIcs\<^footnote>\<open>\<^url>\<open>https://github.com/dagstuhl-publishing/styles\<close>\<close>.
+
\<^item> @{system_option_def "document_bibliography"} explicitly enables the use
of \<^verbatim>\<open>bibtex\<close>; the default is to check the presence of \<^verbatim>\<open>root.bib\<close>, but it
could have a different name.
+ \<^item> @{system_option_def "document_heading_prefix"} specifies a prefix for
+ the {\LaTeX} macro names generated from Isar commands like \<^theory_text>\<open>chapter\<close>,
+ \<^theory_text>\<open>section\<close> etc. The default is \<^verbatim>\<open>isamarkup\<close>, e.g. \<^theory_text>\<open>section\<close> becomes
+ \<^verbatim>\<open>\isamarkupsection\<close>.
+
\<^item> @{system_option_def "threads"} determines the number of worker threads
for parallel checking of theories and proofs. The default \<open>0\<close> means that a
sensible maximum value is determined by the underlying hardware. For