On 05/12/2017 17:21, Makarius wrote:
*** 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.
Thanks for this. Just a bit of context info: this simplifies the creation of documents where only a few key parts of a theory are shown (eg main definitions and thms). This in turn can be used to produce readable documentation for large sessions (like HOL-Analysis).
Tobias
This refers to Isabelle/386a31d6d17a.
An example session is attached.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
