more documentation;
authorwenzelm
Tue Dec 05 16:03:58 2017 +0100 (10 months ago)
changeset 67140386a31d6d17a
parent 67139 8fe0aba577af
child 67141 94fca35f80ab
more documentation;
NEWS
src/Doc/System/Sessions.thy
     1.1 --- a/NEWS	Tue Dec 05 15:55:14 2017 +0100
     1.2 +++ b/NEWS	Tue Dec 05 16:03:58 2017 +0100
     1.3 @@ -68,6 +68,17 @@
     1.4  arguments into this format.
     1.5  
     1.6  
     1.7 +*** Document preparation ***
     1.8 +
     1.9 +* System option "document_tags" specifies a default for otherwise
    1.10 +untagged commands. This is occasionally useful to control the global
    1.11 +visibility of commands via session options (e.g. in ROOT).
    1.12 +
    1.13 +* Document markup commands ('section', 'text' etc.) are implicitly
    1.14 +tagged as "document" and visible by default. This avoids the application
    1.15 +of option "document_tags" to these commands.
    1.16 +
    1.17 +
    1.18  *** HOL ***
    1.19  
    1.20  * SMT module:
     2.1 --- a/src/Doc/System/Sessions.thy	Tue Dec 05 15:55:14 2017 +0100
     2.2 +++ b/src/Doc/System/Sessions.thy	Tue Dec 05 16:03:58 2017 +0100
     2.3 @@ -195,6 +195,10 @@
     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 +
    2.11      \<^item> @{system_option_def "threads"} determines the number of worker threads
    2.12      for parallel checking of theories and proofs. The default \<open>0\<close> means that a
    2.13      sensible maximum value is determined by the underlying hardware. For