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


Attachment: Test_Tags.tar.gz
Description: application/gzip

isabelle-dev mailing list

Reply via email to