When Georg added the ability to assign HTML entities to global math
macros, as cc87f810, a comment in the code said:
syntax: Either
\def\macroname{definition}
or
\def\macroname{definition} requires
or
\def\macroname{definition} requires xmlname
or
\def\macroname{definition} extra xmlname requires
This led me to do something silly, when I tried to add xmlenties for e.g.
\coloneeqq. The line was:
\def\coloneqq{\vcentcolon\kern-7mu=} mathtools
and I changed it to:
\def\coloneqq{\vcentcolon\kern-7mu=} mathtools ≔
But now that is wrong, and the line has to be:
\def\coloneqq{\vcentcolon\kern-7mu=} "" ≔ mathtools
Might it not make more sense to have the options be:
\def\macroname{definition}
\def\macroname{definition} requires
\def\macroname{definition} requires xmlname
\def\macroname{definition} requires xmlname extra
??
So far as I can see, the fourth of these, in whichever version, is never
used in the existing code.
Richard
