[isabelle-dev] NEWS: tag markers with scope (update)

[Makarius]

*** Document preparation ***

* Document markers are formal comments of the form
\<^marker>\<open>marker_body\<close> 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. \<^marker>\<open>contributor arg\<close> or
\<^marker>\<open>license arg\<close> and produce PIDE markup that
can retrieved from the document database.

* Old-style command tags %name are re-interpreted as markers with
proof-scope \<^marker>\<open>tag (proof) name\<close> 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.

* Marker \<^marker>\<open>tag name\<close> does not apply to the proof
of a top-level goal
statement by default (e.g. 'theorem', 'lemma'). This is a subtle change
of semantics wrt. old-style %name.


This refers to Isabelle/d13865c21e36, it is a refinement of the new
marker concept to accomodate HOL-Analysis better -- I have already
updated its tags to the new format in Isabelle/f03a01a18c6e.


	Makarius