[isabelle-dev] NEWS: document_tags

[Makarius]

*** 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.


This refers to Isabelle/386a31d6d17a.

An example session is attached.


	Makarius
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Test_Tags.tar.gz
Type: application/gzip
Size: 56984 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20171205/65d161bf/attachment-0001.bin>