feat: html escape docstrings

[alexjbest]

also fix the escape codes

see https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/ConditionallyCompleteLattice/Basic.html#ciSup_le for examples of why this is needed

[hargoniX]

Thanks!

[acmepjz]

Unfortunately this PR breaks the <url> parsing in markdown.

Could you explain why this was needed (as of Oct. 2023)? Seems that currently it's not needed anymore in your example. I checked the git history of that file in Oct. 2023, and have no idea why it was needed at that time (perhaps because old version of doc-gen4 throws the declaration itself to markdown processor?)

[alexjbest]

Check out https://web.archive.org/web/20230325075237/https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/ConditionallyCompleteLattice/Basic.html#ciSup_le and scroll around a bit. Some parts of the page have completely broken formatting.

…

On Fri, 7 Jun 2024, 10:39 Jz Pan, ***@***.***> wrote: Unfortunately this PR breaks the <url> parsing in markdown. Could you explain why this was needed (as of Oct. 2023)? Seems that currently it's not needed anymore in your example. I checked the git history of that file in Oct. 2023, and have no idea why it was needed at that time (perhaps because old version of doc-gen4 throws the declaration itself to markdown processor?) — Reply to this email directly, view it on GitHub <#157 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAM4HVKETW4Y4Y6REWDCJ33ZGF5T3AVCNFSM6AAAAABI6KJXQCVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDCNJUGQ3TIOBZGQ> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[acmepjz]

Some parts of the page have completely broken formatting.

I see. Seems that some code blocks are randomly duplicated. But I'm not sure this is related to the unescape thing. On the other hand, we come up with another solution https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Contribution.20to.20doc-gen4.3F/near/443537944. It turns out that Lean.Xml.instToStringElement is not appropriate here (or perhaps it's buggy leanprover/lean4#4411). Could you have a loot on it?

[alexjbest]

Unfortunately I don't have time to look at the moment. But if you have an implementation that you've tested works fine on this page and others that have < characters in it's probably fine.