[isabelle-dev] NEWS: document markers

[Makarius]

*** Document preparation ***

* Document markers are formal comments of the form ✐‹marker_body› that
are stripped from document output: the effect is to modify the semantic
presentation context or to emit markup to the PIDE document. Some
predefined markers are taken from the Dublin Core Metadata Initiative,
e.g. ✐‹contributor arg› or ✐‹license arg› and produce PIDE markup that
can retrieved from the document database.

* Old-style command tags %name are re-interpreted as markers ✐‹tag name›
and produce LaTeX environments as before. Potential INCOMPATIBILITY:
multiple markers are composed in canonical order, resulting in a
reversed list of tags in the presentation context.


This refers to Isabelle/82e945d472d5, which also contains some
documentation.

The marker concept opens many possibilities for the near future. For
example tags like "visible", "invisible", "important", "unimportant" may
be re-interpreted as more robust and flexible markers (e.g. with scope
indication: command, proof, section).

Or their could be more metadata to help digesting large libraries with
other tools. Presently there are only a few occurrences of
✐‹contributor› in HOL-Algebra to demonstrate the general idea. It is
technically easy to do more, but it requires a good plan to do what and
how exactly.


	Makarius