+% the string to be typeset by |\xref|. Such references are typeset using
+% |\formatxref|, described below.
+%
+% For references that don't fit into this pattern, there's a more complex
+% definition syntax using |\defxref*|:
+% \begin{grammar}
+% <definition> ::= \[[
+% "\\defxref*"
+% "{" <prefix> "}"
+% "{" <expansion> "}"
+% \]]
+% \end{grammar}
+% The \<expansion> is given four arguments.
+% \begin{itemize}
+% \item |#1| is the name of a macro which should be given two arguments,
+% respectively the reference name and the body of the hyperlink to
+% generate.
+% \item |#2| is the name of a macro to apply to the reference name to typeset
+% the actual reference.
+% \item |#3| is the \<mangle> token, or |\relax|.
+% \item |#4| is the reference name itself.
+% \end{itemize}
+%
+% \DescribeMacro\formatxref
+% Simple references are typeset by calling
+% \syntax{"\\formatxref{"<mangle>"}{"<string>"}{"<label>"}"}, which can do as
+% it pleases: the \<mangle> token is from the |\xref| invocation; the
+% \<string> is category of thing being referred to (as established by
+% |\defxref| below); and \<label> is the label, again from |\xref| . The
+% default behaviour is to print
+% \syntax{<mangle>"{"<string>"}~\\ref{"<label>"}"}, but this can be
+% overridden.
+% (Not quite true: in fact, the default does something better if
+% \package{hyperref} is detected, but the idea is basically the same.)