search

leanprover / doc-gen4

Document Generator for Lean 4
Apache License 2.0
62 stars 41 forks source link

fix: escape html correctly #192

Closed eric-wieser closed 2 months ago

eric-wieser commented 2 months ago

This unreverts #191. See the last commits for the fix, relating to not escaping the content of <script> tags.

Tested on a build on the Batteries docs

hargoniX commented 2 months ago

Checked locally as well, seems to be fine this time.

acmepjz commented 2 months ago

I see. That's why I suggested removing Coe String Html as this will reveal all such potentially buggy implicit conversion from String to Html.

hargoniX commented 2 months ago

I was a little conflicted before because it would be quite a burden to add this all over the place, but now that we have two different constructors and see the effect I do agree that it might be a good idea.

eric-wieser commented 2 months ago

The problem is that removing that coercion effectively removes the <tag>text</tag> syntax. The &#32; issue here is because the custom notation doesn't support escape sequences (it should). The script issue is because HTML is not XML, and so script tags don't contain text nodes; they contain some type of CDATA. Besides teaching the custom syntax to treat <script> differently I don't know a good fix for this.