# HG changeset patch
# User wenzelm
# Date 1638540676 -3600
# Node ID 0ab2ed1489eb32072928ecf58b27ae6519b4b477
# Parent  9e9a308562da1577deb2c0b3844c6f14e7a18ebc
more documentation about document build options;

diff -r 9e9a308562da -r 0ab2ed1489eb src/Doc/System/Presentation.thy
--- 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>
 
 
diff -r 9e9a308562da -r 0ab2ed1489eb src/Doc/System/Sessions.thy
--- 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