*** Document preparation *** * System option "document_tags" specifies alternative command tags. This is occasionally useful to control the global visibility of commands via session options (e.g. in ROOT).
This refers to Isabelle/88b0e63d58a5, which also provides the updated documentation. The motivation is the HOL-Analysis manual, which could use options like this: document_variants = "document:manual=-proof,-ML,-unimportant" document_tags = "theorem%important,corollary%important,proposition%important,%unimportant" This means that the above theorem statements are visible by default, and if their proof is not tagged otherwise it retains its default tagging. In contrast, an explicit "lemma %important" in the text makes its proof also important, and something like "proof %unimportant" will be required to hide it. That is a rather minimal change to the previous version of document_tags, and hopefully sufficient for the release. Here are further spots for improvement (after the release): * improved handling of whitespace surrounding hidden material * improved handling (replacement?) of old (*<*)...(*>*) vs. tags * ways to specify command tags for a whole region of text (maybe just in the Prover IDE, not in the source) Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev