From: Jakub Kądziołka <kuba@kadziolka.net>

Hello,

I have just thought to check how the new HTML presentation handles

\<^bsup>. The answer seems to be "not that well" - see for example

HOL-Library.Ramsey:

https://isabelle.in.tum.de/website-Isabelle2021-RC2/dist/library/HOL/HOL-Library/Ramsey.html

The exponents are no longer raised. This is because the <sup> tag is now

generated inside of a <span class="keyword1"> that gets closed before we

get to the </sup>.

Kind regards,

Jakub Kądziołka

From: Makarius <makarius@sketis.net>

See now

https://isabelle.sketis.net/website-Isabelle2021-RC3/dist/library/HOL/HOL-Library/Ramsey.html

where both the HTML and the HTTPS server are more robust.

Makarius

From: Jakub Kądziołka <kuba@kadziolka.net>

The exponents in lemma nsets_Pi_contra work correctly now, but definition

nsets is still broken - the second underscore in ([_]_) should be in a

superscript. The HTML still isn't nested correctly.

Regards,

Jakub Kądziołka

From: Makarius <makarius@sketis.net>

I have refined this further in

https://isabelle.sketis.net/website-Isabelle2021-RC4/dist/library/HOL/HOL-Library/Ramsey.html

where the control symbols with surrounding markup are printed verbatim (as in

Isabelle/jEdit).

I did not notice the malformed HTML, because I trusted "tidy -errors" on

Ubuntu 20.04 to do a proper check, but apparently it didn't.

The subsequent validator appears to be happy about it as "XHTML 1.0 Strict":

https://validator.w3.org/check?uri=https%3A%2F%2Fisabelle.sketis.net%2Fwebsite-Isabelle2021-RC4%2Fdist%2Flibrary%2FHOL%2FHOL-Library%2FRamsey.html&charset=%28detect+automatically%29&doctype=XHTML+1.0+Strict&group=0&user-agent=W3C_Validator%2F1.3+http%3A%2F%2Fvalidator.w3.org%2Fservices

Overall, we do have a conceptual tension in the concepts of block control

symbols vs. PIDE markup. In the next round this needs to be replaced by

something more smooth, such as a regular control symbol \<^sub> operating on a

cartouche.

Makarius

Last updated: Jan 25 2022 at 02:35 UTC