search

leanprover / doc-gen4

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

fix: escape html correctly #190

Closed eric-wieser closed 2 months ago

eric-wieser commented 2 months ago

The .text constructor was a misnomer, as this was not a "text node" in the sense that HTML/DOM defines the phrase.

This renames text to raw (which it appears is only needed in one place) and adds a new text (with escape-on-output semantics) that is used in almost every other place.

Without this change,

def foo («<script>alert("hello world")</script>» : Nat) : Nat := 0

results in javascript injection.

The instance : ToString Html is removed because this makes it too easy to accidentally doubly-escape something.

acmepjz commented 2 months ago

Do you consider also removing Coe String Html? I don't know if it's implicitly used.

hargoniX commented 2 months ago

Merging this broke the mathlib4_docs site, please fix this, test it and open the PR again.

eric-wieser commented 2 months ago

Merging this broke the mathlib4_docs site, please fix this, test it and open the PR again.

By "broke" do you mean "caused the build to fail" or "produced garbage output"?

hargoniX commented 2 months ago

image

The top bar is now visually broken and using the search feature does not work anymore, probably because some escaping broke stuff. As reported here by users: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Documentation.20loading.20issue/near/443714091

acmepjz commented 2 months ago

I think I can look at this later, but not today...

eric-wieser commented 2 months ago

I fixed this in #192