# HG changeset patch
# User wenzelm
# Date 1412609190 -7200
# Node ID 51adee3ace7b35165677914d44ff818ae72a941d
# Parent  b0fff34d32471f2e123d62e8fc11c00b6d2cdea6
documentation of @{cite} and cite_macro;

diff -r b0fff34d3247 -r 51adee3ace7b src/Doc/Isar_Ref/Document_Preparation.thy
--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Mon Oct 06 16:54:35 2014 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Mon Oct 06 17:26:30 2014 +0200
@@ -127,6 +127,7 @@
     @{antiquotation_def ML_functor} & : & @{text antiquotation} \\
     @{antiquotation_def "file"} & : & @{text antiquotation} \\
     @{antiquotation_def "url"} & : & @{text antiquotation} \\
+    @{antiquotation_def "cite"} & : & @{text antiquotation} \\
   \end{matharray}
 
   The overall content of an Isabelle/Isar theory may alternate between
@@ -180,7 +181,8 @@
       @@{antiquotation ML_functor} options @{syntax text} |
       @@{antiquotation "file"} options @{syntax name} |
       @@{antiquotation file_unchecked} options @{syntax name} |
-      @@{antiquotation url} options @{syntax name}
+      @@{antiquotation url} options @{syntax name} |
+      @@{antiquotation cite} options @{syntax cartouche}? (@{syntax name} + @'and')
     ;
     options: '[' (option * ',') ']'
     ;
@@ -279,6 +281,20 @@
   \item @{text "@{url name}"} produces markup for the given URL, which
   results in an active hyperlink within the text.
 
+  \item @{text "@{cite name}"} produces a citation @{verbatim
+  "\\cite{name}"} in {\LaTeX}, where the name refers to some Bib{\TeX}
+  database entry.
+
+  The variant @{text "@{cite \<open>opt\<close> name}"} produces @{verbatim
+  "\\cite[opt]{name}"} with some free-form optional argument. Multiple names
+  are output with commas, e.g. @{text "@{cite foo \<AND> bar}"} becomes
+  @{verbatim "\\cite{foo,bar}"}.
+
+  The {\LaTeX} macro name is determined by the antiquotation option
+  @{antiquotation_option_def cite_macro}, or the configuration option
+  @{attribute cite_macro} in the context. For example, @{text "@{cite
+  [cite_macro = nocite] foobar}"} produces @{verbatim "\\nocite{foobar}"}.
+
   \end{description}
 *}