NEWS
changeset 70140 d13865c21e36
parent 70127 538d9854ca2f
child 70143 0cc7fe616924
     1.1 --- a/NEWS	Fri Apr 12 22:52:00 2019 +0200
     1.2 +++ b/NEWS	Fri Apr 12 22:57:17 2019 +0200
     1.3 @@ -121,10 +121,15 @@
     1.4  e.g. \<^marker>\<open>contributor arg\<close> or \<^marker>\<open>license arg\<close> and produce PIDE markup that
     1.5  can retrieved from the document database.
     1.6  
     1.7 -* Old-style command tags %name are re-interpreted as markers \<^marker>\<open>tag name\<close>
     1.8 -and produce LaTeX environments as before. Potential INCOMPATIBILITY:
     1.9 -multiple markers are composed in canonical order, resulting in a
    1.10 -reversed list of tags in the presentation context.
    1.11 +* Old-style command tags %name are re-interpreted as markers with
    1.12 +proof-scope \<^marker>\<open>tag (proof) name\<close> and produce LaTeX environments as
    1.13 +before. Potential INCOMPATIBILITY: multiple markers are composed in
    1.14 +canonical order, resulting in a reversed list of tags in the
    1.15 +presentation context.
    1.16 +
    1.17 +* Marker \<^marker>\<open>tag name\<close> does not apply to the proof of a top-level goal
    1.18 +statement by default (e.g. 'theorem', 'lemma'). This is a subtle change
    1.19 +of semantics wrt. old-style %name.
    1.20  
    1.21  * Document antiquotation option "cartouche" indicates if the output
    1.22  should be delimited as cartouche; this takes precedence over the