# 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>\contributor arg\ or \<^marker>\license arg\ and produce PIDE markup that can retrieved from the document database. -* Old-style command tags %name are re-interpreted as markers \<^marker>\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. +* Old-style command tags %name are re-interpreted as markers with +proof-scope \<^marker>\tag (proof) 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. + +* Marker \<^marker>\tag name\ 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') ')' \ \<^descr> \\<^marker>\title arg\\, \\<^marker>\creator arg\\, \\<^marker>\contributor arg\\, \\<^marker>\date arg\\, @@ -532,12 +534,19 @@ \<^theory_text>\keywords\ declaration of a command, and the system option @{system_option_ref document_tags}. + The optional \scope\ tells how far the tagging is applied to subsequent + proof structure: ``\<^theory_text>\("proof")\'' means it applies to the following proof + text, and ``\<^theory_text>\(command)\'' means it only applies to the current command. + The default within a proof body is ``\<^theory_text>\("proof")\'', but for toplevel goal + statements it is ``\<^theory_text>\(command)\''. Thus a \tag\ marker for \<^theory_text>\theorem\, + \<^theory_text>\lemma\ etc. does \emph{not} affect its proof by default. + An old-style command tag \<^verbatim>\%\\name\ is treated like a document marker - \\<^marker>\tag name\\: 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: + \\<^marker>\tag (proof) name\\: 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}