# HG changeset patch
# User wenzelm
# Date 1555102637 -7200
# Node ID d13865c21e3637dc8c9af6e8fcf69e1b11c9f4e8
# Parent  fd4960dfad2a2625e5f2f6faac1f66d73c326869
updated documentation;

diff -r fd4960dfad2a -r d13865c21e36 NEWS
--- a/NEWS	Fri Apr 12 22:52:00 2019 +0200
+++ b/NEWS	Fri Apr 12 22:57:17 2019 +0200
@@ -121,10 +121,15 @@
 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 \<^marker>\<open>tag 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.
+* 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.
 
 * Document antiquotation option "cartouche" indicates if the output
 should be delimited as cartouche; this takes precedence over the
diff -r fd4960dfad2a -r d13865c21e36 src/Doc/Isar_Ref/Document_Preparation.thy
--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Fri Apr 12 22:52:00 2019 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Fri Apr 12 22:57:17 2019 +0200
@@ -515,7 +515,9 @@
      @@{document_marker_def license} |
      @@{document_marker_def description}) @{syntax embedded}
     ;
-    @@{document_marker_def tag} @{syntax name}
+    @@{document_marker_def tag} (scope?) @{syntax name}
+    ;
+    scope: '(' ('proof' | 'command') ')'
   \<close>
 
     \<^descr> \<open>\<^marker>\<open>title arg\<close>\<close>, \<open>\<^marker>\<open>creator arg\<close>\<close>, \<open>\<^marker>\<open>contributor arg\<close>\<close>, \<open>\<^marker>\<open>date arg\<close>\<close>,
@@ -532,12 +534,19 @@
     \<^theory_text>\<open>keywords\<close> declaration of a command, and the system option
     @{system_option_ref document_tags}.
 
+    The optional \<open>scope\<close> tells how far the tagging is applied to subsequent
+    proof structure: ``\<^theory_text>\<open>("proof")\<close>'' means it applies to the following proof
+    text, and ``\<^theory_text>\<open>(command)\<close>'' means it only applies to the current command.
+    The default within a proof body is ``\<^theory_text>\<open>("proof")\<close>'', but for toplevel goal
+    statements it is ``\<^theory_text>\<open>(command)\<close>''. Thus a \<open>tag\<close> marker for \<^theory_text>\<open>theorem\<close>,
+    \<^theory_text>\<open>lemma\<close> etc. does \emph{not} affect its proof by default.
+
     An old-style command tag \<^verbatim>\<open>%\<close>\<open>name\<close> is treated like a document marker
-    \<open>\<^marker>\<open>tag name\<close>\<close>: the list of command tags precedes the list of document
-    markers. The head of the resulting tags in the presentation context is
-    turned into {\LaTeX} environments to modify the type-setting. The
-    following tags are pre-declared for certain classes of commands, and serve
-    as default markup for certain kinds of commands:
+    \<open>\<^marker>\<open>tag (proof) name\<close>\<close>: the list of command tags precedes the list of
+    document markers. The head of the resulting tags in the presentation
+    context is turned into {\LaTeX} environments to modify the type-setting.
+    The following tags are pre-declared for certain classes of commands, and
+    serve as default markup for certain kinds of commands:
 
     \<^medskip>
     \begin{tabular}{ll}