--- a/src/Doc/System/Sessions.thy Mon Jun 07 09:36:21 2021 +0200
+++ b/src/Doc/System/Sessions.thy Mon Jun 07 11:42:05 2021 +0200
@@ -201,8 +201,9 @@
info, see also \secref{sec:info}.
\<^item> @{system_option_def "document"} controls document output for a
- particular session or theory; \<^verbatim>\<open>document=pdf\<close> means enabled,
- \<^verbatim>\<open>document=false\<close> means disabled (especially for particular theories).
+ particular session or theory; \<^verbatim>\<open>document=pdf\<close> or \<^verbatim>\<open>document=true\<close> means
+ enabled, \<^verbatim>\<open>document=""\<close> or \<^verbatim>\<open>document=false\<close> means disabled (especially
+ for particular theories).
\<^item> @{system_option_def "document_output"} specifies an alternative
directory for generated output of the document preparation system; the
@@ -278,7 +279,8 @@
\<^item> @{system_option_def system_log} specifies an optional log file for
low-level messages produced by \<^ML>\<open>Output.system_message\<close> in
- Isabelle/ML; ``\<^verbatim>\<open>-\<close>'' refers to console progress of the build job.
+ Isabelle/ML; the value ``\<^verbatim>\<open>true\<close>'' refers to console progress of the build
+ job.
\<^item> @{system_option_def "system_heaps"} determines the directories for
session heap images: \<^path>\<open>$ISABELLE_HEAPS\<close> is the user directory and
@@ -410,11 +412,12 @@
The build process depends on additional options
(\secref{sec:system-options}) that are passed to the prover eventually. The
settings variable @{setting_ref ISABELLE_BUILD_OPTIONS} allows to provide
- additional defaults, e.g.\ \<^verbatim>\<open>ISABELLE_BUILD_OPTIONS="document=pdf threads=4"\<close>.
- Moreover, the environment of system build options may be augmented on the
- command line via \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close> or \<^verbatim>\<open>-o\<close>~\<open>name\<close>, which abbreviates
- \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=true\<close> for Boolean options. Multiple occurrences of \<^verbatim>\<open>-o\<close> on
- the command-line are applied in the given order.
+ additional defaults, e.g.\ \<^verbatim>\<open>ISABELLE_BUILD_OPTIONS="document=pdf
+ threads=4"\<close>. Moreover, the environment of system build options may be
+ augmented on the command line via \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close> or \<^verbatim>\<open>-o\<close>~\<open>name\<close>,
+ which abbreviates \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=true\<close> for Boolean or string options.
+ Multiple occurrences of \<^verbatim>\<open>-o\<close> on the command-line are applied in the given
+ order.
\<^medskip>
Option \<^verbatim>\<open>-P\<close> enables PDF/HTML presentation in the given directory, where
@@ -496,7 +499,7 @@
\<^smallskip>
Build all sessions with HTML browser info and PDF document preparation:
- @{verbatim [display] \<open>isabelle build -a -o browser_info -o document=pdf\<close>}
+ @{verbatim [display] \<open>isabelle build -a -o browser_info -o document\<close>}
\<^smallskip>
Build all sessions with a maximum of 8 parallel prover processes and 4