update documentation: prefer control-symbol-cartouche form of "cite" antiquotations;

--- a/NEWS	Sat Jan 14 22:37:15 2023 +0100
+++ b/NEWS	Sat Jan 14 23:50:13 2023 +0100
@@ -22,7 +22,20 @@
 Isabelle/jEdit Document panel.
 
 * Support for more "cite" antiquotations, notably for \nocite and
-natbib's \citet / \citep.
+natbib's \citet / \citep. The antiquotation syntax now supports
+control-symbol-cartouche form, with an embedded argument:
+\<^cite>\<open>arg\<close>. The embedded argument syntax supports both the optional
+and mandatory argument of the underlying \cite-like macro.
+
+Examples:
+
+  \<^cite>\<open>\<open>\S1.2\<close> in "isabelle-system"\<close>
+  \<^cite>\<open>"isabelle-system" and "isabelle-jedit"\<close>
+  \<^nocite>\<open>"isabelle-isar-ref"\<close>
+
+The command-line tool "isabelle update -u cite_commands -l HOL" helps to
+update former uses of raw \cite commands or old @{cite "name"}
+antiquotations.
 
 
 *** HOL ***

--- a/lib/texinputs/isabellesym.sty	Sat Jan 14 22:37:15 2023 +0100
+++ b/lib/texinputs/isabellesym.sty	Sat Jan 14 23:50:13 2023 +0100
@@ -495,3 +495,8 @@
 \newcommand{\isactrlifUNDERSCOREmacos}{\isakeywordcontrol{if{\isacharunderscore}macos}}
 \newcommand{\isactrlifUNDERSCOREwindows}{\isakeywordcontrol{if{\isacharunderscore}windows}}
 \newcommand{\isactrlifUNDERSCOREunix}{\isakeywordcontrol{if{\isacharunderscore}unix}}
+
+\newcommand{\isactrlcite}{\isakeywordcontrol{cite}}
+\newcommand{\isactrlnocite}{\isakeywordcontrol{nocite}}
+\newcommand{\isactrlcitet}{\isakeywordcontrol{citet}}
+\newcommand{\isactrlcitep}{\isakeywordcontrol{citep}}

--- 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