[isabelle-dev] Potential HTML generation bug

MACKENZIE Carlin s1724780 at sms.ed.ac.uk
Sat Jan 23 19:31:01 CET 2021


Dear all,

I’ve recently noticed that some HTML output has highly nested nodes which seem to be in error. The most extreme example of this I have found is in:
https://devel.isa-afp.org/browser_info/current/AFP/MonoidalCategory/MonoidalCategory.html

Some symbols are wrapped in 591 nested <span class="keyword1"> </span>. They are listed in this validation of the page https://validator.w3.org/nu/?doc=https%3A%2F%2Fdevel.isa-afp.org%2Fbrowser_info%2Fcurrent%2FAFP%2FMonoidalCategory%2FMonoidalCategory.html .

Regards,
Carlin MacKenzie
The University of Edinburgh

The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20210123/a925dfd4/attachment.htm>


More information about the isabelle-dev mailing list