A broken generated HTML theory in non-Unicode mode

[binghe]

Hi,

It seems that for each core theory there are two HTML pages generated in the help page. One is that you directly click the theory names from the HOL Reference Page (help/index.html), the other is that you first go to the Theory Graph (help/theorygraph/theories.html) and then click the graph nodes. The first one contains definitions and theorems with Unicode letters, and the second one doesn't use Unicode. I would say it's not bad to have two different HTML outputs for the same theory file.

But in cardinalTheory, the abbreviation symbol of cardlt (<</=) has caused problems with HTML because part of it looks like a HTML tag:

val _ = set_fixity "<</=" (Infix(NONASSOC, 450));

val _ = Unicode.unicode_version {u = UTF8.chr 0x227A, tmnm = "<</="};
val _ = TeX_notation {hol = "<</=",          TeX = ("\\ensuremath{\\prec}", 1)};
val _ = TeX_notation {hol = UTF8.chr 0x227A, TeX = ("\\ensuremath{\\prec}", 1)};

val _ = overload_on ("cardlt", ``\s1 s2. ~(cardleq s2 s1)``); (* cardlt *)
val _ = overload_on ("<</=", ``cardlt``);

And if you open the non-Unicode version of HTML page of cardinalTheory, you can see something like this:

Either we fix the HTML-generation code to escape the problematic characters (better, but I have no idea where is the related SML code), or we modify the symbols of cardlt (but there could be more such cases that I haven't seen).

Chun

[mn200]

The HTML printing is done in src/parse/Hol_pp.sml.

[binghe]

The HTML printing is done in src/parse/Hol_pp.sml.

Thanks. Then I will try to fix this issue.