[isabelle-dev] NEWS: document_tags (update)

[Makarius]

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