The Coq mailing list

["N. Raghavendra" <raghu AT hri.res.in>]

I tried to validate the Coqdoc output from some of my files with respect
to the XHML 1.0 Strict DTD, and found that all of them were OK except
for one small point.  If I use an apostrophe character in the name of
some object, Coqdoc writes it as <a name="foo'">...</a>.  This breaks
validation because the apostrophe isn't a valid name character in XML.
Similarly, in the index file generated by Coqdoc, there are things like
<a href="index.html#global_*">other</a>.  Again, the asterisk isn't a
valid name character in XML.  Right now, I am doing something like

s|<a name="([^']+)'">|<a name="\1PRIME">|g
s|<a href="([^']+)'">|<a href="\1PRIME">|g

s|<a name="([^']+)\*">|<a name="\1STAR">|g
s|<a href="([^']+)\*">|<a href="\1STAR">|g

in a sed script to replace the problem characters in the generated HTML
files with suitable strings, and change links to the anchors
accordingly.  I wonder if this kind of sanitising of name attribute
values could be incorporated into Coqdoc.

Cheers,
Raghu.

-- 
N. Raghavendra 
<raghu AT hri.res.in>,
 http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/