src/Doc/Isar_Ref/Document_Preparation.thy

--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Sat Jan 14 22:37:15 2023 +0100
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Sat Jan 14 23:50:13 2023 +0100
@@ -221,7 +221,8 @@
       @@{antiquotation "file"} options @{syntax name} |
       @@{antiquotation dir} options @{syntax name} |
       @@{antiquotation url} options @{syntax embedded} |
-      @@{antiquotation cite} options @{syntax cartouche}? (@{syntax name} + @'and')
+      (@@{antiquotation cite} | @@{antiquotation nocite} |
+       @@{antiquotation citet} | @@{antiquotation citep}) @{syntax embedded}
     ;
     styles: '(' (style + ',') ')'
     ;
@@ -344,18 +345,26 @@
   \<^descr> \<open>@{url name}\<close> produces markup for the given URL, which results in an
   active hyperlink within the text.
 
-  \<^descr> \<open>@{cite name}\<close> produces a citation \<^verbatim>\<open>\cite{name}\<close> in {\LaTeX}, where the
-  name refers to some Bib{\TeX} database entry. This is only checked in
-  batch-mode session builds.
+  \<^descr> \<open>@{cite arg}\<close> produces the Bib{\TeX} citation macro \<^verbatim>\<open>\cite[...]{...}\<close>
+  with its optional and mandatory argument. The analogous \<^verbatim>\<open>\nocite\<close>, and the
+  \<^verbatim>\<open>\citet\<close> and \<^verbatim>\<open>\citep\<close> variants from the \<^verbatim>\<open>natbib\<close>
+  package\<^footnote>\<open>\<^url>\<open>https://ctan.org/pkg/natbib\<close>\<close> are supported as well. Further
+  versions can be defined easily in Isabelle/ML, by imitating the ML
+  definitions behind the existing antiquotations.
 
-  The variant \<open>@{cite \<open>opt\<close> name}\<close> produces \<^verbatim>\<open>\cite[opt]{name}\<close> with some
-  free-form optional argument. Multiple names are output with commas, e.g.
-  \<open>@{cite foo \<AND> bar}\<close> becomes \<^verbatim>\<open>\cite{foo,bar}\<close>.
+  The argument syntax is uniform for all variants and is usually presented in
+  control-symbol-cartouche form: \<open>\<^cite>\<open>arg\<close>\<close>. The formal syntax of the
+  nested argument language is defined as follows: \<^rail>\<open>arg: (embedded
+  @'in')? (name + 'and')\<close>
 
-  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, \<open>@{cite [cite_macro =
-  nocite] foobar}\<close> produces \<^verbatim>\<open>\nocite{foobar}\<close>.
+  Here the embedded text is free-form {\LaTeX}, which becomes the optional
+  argument of the \<^verbatim>\<open>\cite\<close> macro. The named items are Bib{\TeX} database
+  entries and become the mandatory argument (separated by comma).
+
+  The validity of Bib{\TeX} database entries is only partially checked in
+  Isabelle/PIDE, when the corresponding \<^verbatim>\<open>.bib\<close> files are open. Ultimately,
+  the \<^verbatim>\<open>bibtex\<close> program will complain about bad input in final document
+  preparation.
 
   \<^descr> @{command "print_antiquotations"} prints all document antiquotations that
   are defined in the current context; the ``\<open>!\<close>'' option indicates extra