updated documentation;
authorwenzelm
Tue Jun 26 19:16:14 2018 +0200 (17 months ago)
changeset 6851388b0e63d58a5
parent 68512 16ae55c77bcb
child 68514 b20980997cd2
updated documentation;
NEWS
src/Doc/System/Sessions.thy
     1.1 --- a/NEWS	Tue Jun 26 19:03:13 2018 +0200
     1.2 +++ b/NEWS	Tue Jun 26 19:16:14 2018 +0200
     1.3 @@ -151,9 +151,9 @@
     1.4  theory Pure. Thus elementary antiquotations may be used in markup
     1.5  commands (e.g. 'chapter', 'section', 'text') and formal comments.
     1.6  
     1.7 -* System option "document_tags" specifies a default for otherwise
     1.8 -untagged commands. This is occasionally useful to control the global
     1.9 -visibility of commands via session options (e.g. in ROOT).
    1.10 +* System option "document_tags" specifies alternative command tags. This
    1.11 +is occasionally useful to control the global visibility of commands via
    1.12 +session options (e.g. in ROOT).
    1.13  
    1.14  * Document markup commands ('section', 'text' etc.) are implicitly
    1.15  tagged as "document" and visible by default. This avoids the application
     2.1 --- a/src/Doc/System/Sessions.thy	Tue Jun 26 19:03:13 2018 +0200
     2.2 +++ b/src/Doc/System/Sessions.thy	Tue Jun 26 19:16:14 2018 +0200
     2.3 @@ -199,9 +199,11 @@
     2.4      possible to use different document variant names (without tags) for
     2.5      different document root entries, see also \secref{sec:tool-document}.
     2.6  
     2.7 -    \<^item> @{system_option_def "document_tags"} specifies a default for otherwise
     2.8 -    untagged commands. This is occasionally useful to control the global
     2.9 -    visibility of commands via session options (e.g. in \<^verbatim>\<open>ROOT\<close>).
    2.10 +    \<^item> @{system_option_def "document_tags"} specifies alternative command tags
    2.11 +    as a comma-separated list of items: either ``\<open>command\<close>\<^verbatim>\<open>%\<close>\<open>tag\<close>'' for a
    2.12 +    specific command, or ``\<^verbatim>\<open>%\<close>\<open>tag\<close>'' as default for all other commands. This
    2.13 +    is occasionally useful to control the global visibility of commands via
    2.14 +    session options (e.g.\ in \<^verbatim>\<open>ROOT\<close>).
    2.15  
    2.16      \<^item> @{system_option_def "threads"} determines the number of worker threads
    2.17      for parallel checking of theories and proofs. The default \<open>0\<close> means that a