# HG changeset patch
# User wenzelm
# Date 1512486238 -3600
# Node ID 386a31d6d17aa59eab7a5b66a2bacf2b4e4932cc
# Parent  8fe0aba577afc5f42274768ab9f56f2a1ccc52a5
more documentation;

diff -r 8fe0aba577af -r 386a31d6d17a NEWS
--- 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:
diff -r 8fe0aba577af -r 386a31d6d17a src/Doc/System/Sessions.thy
--- 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