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 <>

I have just thought to check how the new HTML presentation handles
\<^bsup>. The answer seems to be "not that well" - see for example

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 <>
See now
where both the HTML and the HTTPS server are more robust.


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

From: Jakub Kądziołka <>
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.

Jakub Kądziołka

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

From: Makarius <>
I have refined this further in
where the control symbols with surrounding markup are printed verbatim (as in

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":

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


Last updated: Dec 05 2021 at 22:18 UTC