Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Missing commands in generated AFP websites

Email Gateway (Dec 14 2021 at 16:07):

From: Dmitriy Traytel <traytel@di.ku.dk>
Hi all, mainly AFP editors,

not sure if this is related to the new release of the AFP, but I have just noticed that the datatype (and nominal_datatype) commands are missing from the generated websites for several entries (I looked at MFODL_Monitor_Optimized, from which the attached screenshot comes, and Incompleteness: look for tm and fm in https://www.isa-afp.org/browser_info/current/AFP/Incompleteness/SyntaxN.html). This seems to only affect the Safari web-browser (Chrome shows the commands).

In contrast, things also look fine from Safari for websites in the distribution, e.g.,

https://isabelle.in.tum.de/library/HOL/HOL-Datatype_Examples/Misc_Datatype.html

Dmitriy

[cid:AA1AEEC4-CA1B-4270-BA37-E0E21FD9A218]
no-datatype.png

Email Gateway (Dec 14 2021 at 16:44):

From: Fabian Huch <huch@in.tum.de>
The HTML there is quite deeply nested, since there is a <span> element
for every foundational entity.

The Safari rendering apparently chokes on that if the tree is too large
(hence it works for some examples); if you inspect the HTML, you will
see that they are not missing.

Not sure how to approach this. Maybe file a bug report for Safari?

Fabian
no-datatype.png

Last updated: Jan 04 2025 at 20:18 UTC