# HG changeset patch
# User wenzelm
# Date 1530033374 -7200
# Node ID 88b0e63d58a5558b5c7af1f881447488171d5c78
# Parent  16ae55c77bcb1ad372daa61d89c7e09ed760ac34
updated documentation;

diff -r 16ae55c77bcb -r 88b0e63d58a5 NEWS
--- a/NEWS	Tue Jun 26 19:03:13 2018 +0200
+++ b/NEWS	Tue Jun 26 19:16:14 2018 +0200
@@ -151,9 +151,9 @@
 theory Pure. Thus elementary antiquotations may be used in markup
 commands (e.g. 'chapter', 'section', 'text') and formal comments.
 
-* 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).
+* System option "document_tags" specifies alternative command tags. 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
diff -r 16ae55c77bcb -r 88b0e63d58a5 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Tue Jun 26 19:03:13 2018 +0200
+++ b/src/Doc/System/Sessions.thy	Tue Jun 26 19:16:14 2018 +0200
@@ -199,9 +199,11 @@
     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 "document_tags"} specifies alternative command tags
+    as a comma-separated list of items: either ``\<open>command\<close>\<^verbatim>\<open>%\<close>\<open>tag\<close>'' for a
+    specific command, or ``\<^verbatim>\<open>%\<close>\<open>tag\<close>'' as default for all other 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