updated documentation;
authorwenzelm
Fri Apr 12 22:57:17 2019 +0200 (5 months ago)
changeset 70140d13865c21e36
parent 70139 fd4960dfad2a
child 70141 5965a0a60c85
updated documentation;
NEWS
src/Doc/Isar_Ref/Document_Preparation.thy
     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
     2.1 --- a/src/Doc/Isar_Ref/Document_Preparation.thy	Fri Apr 12 22:52:00 2019 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Fri Apr 12 22:57:17 2019 +0200
     2.3 @@ -515,7 +515,9 @@
     2.4       @@{document_marker_def license} |
     2.5       @@{document_marker_def description}) @{syntax embedded}
     2.6      ;
     2.7 -    @@{document_marker_def tag} @{syntax name}
     2.8 +    @@{document_marker_def tag} (scope?) @{syntax name}
     2.9 +    ;
    2.10 +    scope: '(' ('proof' | 'command') ')'
    2.11    \<close>
    2.12  
    2.13      \<^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>,
    2.14 @@ -532,12 +534,19 @@
    2.15      \<^theory_text>\<open>keywords\<close> declaration of a command, and the system option
    2.16      @{system_option_ref document_tags}.
    2.17  
    2.18 +    The optional \<open>scope\<close> tells how far the tagging is applied to subsequent
    2.19 +    proof structure: ``\<^theory_text>\<open>("proof")\<close>'' means it applies to the following proof
    2.20 +    text, and ``\<^theory_text>\<open>(command)\<close>'' means it only applies to the current command.
    2.21 +    The default within a proof body is ``\<^theory_text>\<open>("proof")\<close>'', but for toplevel goal
    2.22 +    statements it is ``\<^theory_text>\<open>(command)\<close>''. Thus a \<open>tag\<close> marker for \<^theory_text>\<open>theorem\<close>,
    2.23 +    \<^theory_text>\<open>lemma\<close> etc. does \emph{not} affect its proof by default.
    2.24 +
    2.25      An old-style command tag \<^verbatim>\<open>%\<close>\<open>name\<close> is treated like a document marker
    2.26 -    \<open>\<^marker>\<open>tag name\<close>\<close>: the list of command tags precedes the list of document
    2.27 -    markers. The head of the resulting tags in the presentation context is
    2.28 -    turned into {\LaTeX} environments to modify the type-setting. The
    2.29 -    following tags are pre-declared for certain classes of commands, and serve
    2.30 -    as default markup for certain kinds of commands:
    2.31 +    \<open>\<^marker>\<open>tag (proof) name\<close>\<close>: the list of command tags precedes the list of
    2.32 +    document markers. The head of the resulting tags in the presentation
    2.33 +    context is turned into {\LaTeX} environments to modify the type-setting.
    2.34 +    The following tags are pre-declared for certain classes of commands, and
    2.35 +    serve as default markup for certain kinds of commands:
    2.36  
    2.37      \<^medskip>
    2.38      \begin{tabular}{ll}