[isabelle-dev] NEWS: document_tags (update)
makarius at sketis.net
Tue Jun 26 20:01:23 CEST 2018
*** 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"
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)
More information about the isabelle-dev