Re: [isabelle] Isabelle2021-RC2: slight regression in HTML output

On 24/01/2021 23:20, Jakub Kądziołka wrote:
> On Sun Jan 24, 2021 at 8:08 PM CET, Makarius wrote:
>> On 13/01/2021 00:29, Jakub Kądziołka wrote:
>>> 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:
>> See now
>> where both the HTML and the HTTPS server are more robust.
> 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.

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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.