--- a/src/Doc/Isar_Ref/Document_Preparation.thy Sun Oct 18 17:24:24 2015 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Sun Oct 18 18:09:48 2015 +0200
@@ -129,15 +129,24 @@
antiquotations are checked within the current theory or proof
context.
+ \<^medskip>
+ Antiquotations are in general written @{verbatim "@{"}@{text "name
+ [options] arguments"}@{verbatim "}"}. The short form @{verbatim
+ "\<^control>"}@{text "\<open>argument\<close>"} (without surrounding @{verbatim
+ "@{"}@{text "\<dots>"}@{verbatim "}"}) works where the name is a single control
+ symbol and the argument a single cartouche.
+
@{rail \<open>
@@{command print_antiquotations} ('!'?)
+ ;
+ @{syntax_def antiquotation}:
+ '@{' antiquotation_body '}' |
+ @{syntax_ref control_symbol} @{syntax_ref cartouche}
\<close>}
%% FIXME less monolithic presentation, move to individual sections!?
@{rail \<open>
- '@{' antiquotation '}'
- ;
- @{syntax_def antiquotation}:
+ @{syntax_def antiquotation_body}:
@@{antiquotation theory} options @{syntax name} |
@@{antiquotation thm} options styles @{syntax thmrefs} |
@@{antiquotation lemma} options @{syntax prop} @'by' @{syntax method} @{syntax method}? |
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy Sun Oct 18 17:24:24 2015 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Sun Oct 18 18:09:48 2015 +0200
@@ -114,6 +114,7 @@
@{syntax_def cartouche} & = & @{verbatim "\<open>"} @{text "\<dots>"} @{verbatim "\<close>"} \\
@{syntax_def verbatim} & = & @{verbatim "{*"} @{text "\<dots>"} @{verbatim "*}"} \\[1ex]
+ @{text control_symbol} & = & @{verbatim \<open>\\<close>}@{verbatim "<^"}@{text ident}@{verbatim ">"} \\
@{text letter} & = & @{text "latin | "}@{verbatim \<open>\\<close>}@{verbatim "<"}@{text latin}@{verbatim ">"}@{text " | "}@{verbatim \<open>\\<close>}@{verbatim "<"}@{text "latin latin"}@{verbatim ">"}@{text " | greek |"} \\
@{text subscript} & = & @{verbatim "\<^sub>"} \\
@{text quasiletter} & = & @{text "letter | digit | "}@{verbatim "_"}@{text " | "}@{verbatim "'"} \\