--- a/NEWS Tue Dec 05 15:55:14 2017 +0100
+++ b/NEWS Tue Dec 05 16:03:58 2017 +0100
@@ -68,6 +68,17 @@
arguments into this format.
+*** Document preparation ***
+
+* System option "document_tags" specifies a default for otherwise
+untagged commands. This is occasionally useful to control the global
+visibility of commands via session options (e.g. in ROOT).
+
+* Document markup commands ('section', 'text' etc.) are implicitly
+tagged as "document" and visible by default. This avoids the application
+of option "document_tags" to these commands.
+
+
*** HOL ***
* SMT module:
--- a/src/Doc/System/Sessions.thy Tue Dec 05 15:55:14 2017 +0100
+++ b/src/Doc/System/Sessions.thy Tue Dec 05 16:03:58 2017 +0100
@@ -195,6 +195,10 @@
possible to use different document variant names (without tags) for
different document root entries, see also \secref{sec:tool-document}.
+ \<^item> @{system_option_def "document_tags"} specifies a default for otherwise
+ untagged commands. This is occasionally useful to control the global
+ visibility of commands via session options (e.g. in \<^verbatim>\<open>ROOT\<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