# 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 "\argument\"} (without surrounding @{verbatim + "@{"}@{text "\"}@{verbatim "}"}) works where the name is a single control + symbol and the argument a single cartouche. + @{rail \ @@{command print_antiquotations} ('!'?) + ; + @{syntax_def antiquotation}: + '@{' antiquotation_body '}' | + @{syntax_ref control_symbol} @{syntax_ref cartouche} \} %% FIXME less monolithic presentation, move to individual sections!? @{rail \ - '@{' 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 "\"} @{text "\"} @{verbatim "\"} \\ @{syntax_def verbatim} & = & @{verbatim "{*"} @{text "\"} @{verbatim "*}"} \\[1ex] + @{text control_symbol} & = & @{verbatim \\\}@{verbatim "<^"}@{text ident}@{verbatim ">"} \\ @{text letter} & = & @{text "latin | "}@{verbatim \\\}@{verbatim "<"}@{text latin}@{verbatim ">"}@{text " | "}@{verbatim \\\}@{verbatim "<"}@{text "latin latin"}@{verbatim ">"}@{text " | greek |"} \\ @{text subscript} & = & @{verbatim "\<^sub>"} \\ @{text quasiletter} & = & @{text "letter | digit | "}@{verbatim "_"}@{text " | "}@{verbatim "'"} \\