# HG changeset patch
# User wenzelm
# Date 1445184588 -7200
# Node ID 6458760261caa35132190d6cdd1e42f7e066a4d8
# Parent  9d4c08af61b8bf2b4841c07d7d58cc1f630cc5b6
more documentation;

diff -r 9d4c08af61b8 -r 6458760261ca src/Doc/Isar_Ref/Document_Preparation.thy
--- 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}? |
diff -r 9d4c08af61b8 -r 6458760261ca src/Doc/Isar_Ref/Outer_Syntax.thy
--- 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 "'"} \\