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:
>>>
>>> https://isabelle.in.tum.de/website-Isabelle2021-RC2/dist/library/HOL/HOL-Library/Ramsey.html
>>
>> 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.
> 
> 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
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




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