--- a/src/Doc/System/Sessions.thy Tue May 18 21:09:51 2021 +0200
+++ b/src/Doc/System/Sessions.thy Tue May 18 22:02:21 2021 +0200
@@ -238,6 +238,12 @@
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_preprocessor"} specifies the name of an
+ executable that is run within the document output directory, after
+ preparing the document sources and before the actual build process. This
+ allows to apply adhoc patches, without requiring a separate \<^verbatim>\<open>build\<close>
+ script.
+
\<^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