Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2021-RC2: slight regression in HTML ou...


view this post on Zulip Email Gateway (Jan 12 2021 at 23:34):

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

view this post on Zulip Email Gateway (Jan 24 2021 at 19:08):

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

view this post on Zulip Email Gateway (Jan 24 2021 at 22:22):

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

view this post on Zulip Email Gateway (Feb 01 2021 at 14:59):

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: Dec 05 2021 at 22:18 UTC