diff -r 5b49c650d413 -r 72900f34dbb3 src/Doc/System/Sessions.thy
--- 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