feat: Better equation Handling

The equation content is now escaped, furthermore there is a limit
for the length of an equation so we don't just fill everything with
uselessly big equations nobody can read anyways.
main
Henrik Böving 2022-02-20 13:45:18 +01:00
parent 87a8b8feb0
commit b87c1cc1de
3 changed files with 42 additions and 10 deletions

View File

@ -66,7 +66,7 @@ def splitWhitespaces (s : String) : (String × String × String) := Id.run do
partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do
match i with
| TaggedText.text t => pure #[t]
| TaggedText.text t => pure #[Html.escape t]
| TaggedText.append tt => tt.foldlM (λ acc t => do pure $ acc ++ (←infoFormatToHtml t)) #[]
| TaggedText.tag a t =>
match a.info.val.info with
@ -75,7 +75,7 @@ partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do
| Expr.const name _ _ =>
match t with
| TaggedText.text t =>
let (front, t, back) := splitWhitespaces t
let (front, t, back) := splitWhitespaces $ Html.escape t
let elem := Html.element "a" true #[("href", ←declNameToLink name)] #[t]
pure #[Html.text front, elem, Html.text back]
| _ =>

View File

@ -7,17 +7,32 @@ namespace Output
open scoped DocGen4.Jsx
open Lean Widget
/- This is basically an arbitrary number that seems to work okay. -/
def equationLimit : Nat := 200
def equationToHtml (c : CodeWithInfos) : HtmlM Html := do
pure <li «class»="equation">[←infoFormatToHtml c]</li>
def equationsToHtml (i : DefinitionInfo) : HtmlM (Array Html) := do
if let some eqs := i.equations then
let equationsHtml ← eqs.mapM equationToHtml
let filteredEquationsHtml := equationsHtml.filter (λ eq => eq.textLength < equationLimit)
if equationsHtml.size ≠ filteredEquationsHtml.size then
pure #[
<details>
<summary>Equations</summary>
<ul «class»="equations">
[equationsHtml]
<li «class»="equation">One or more equations did not get rendered due to their size.</li>
[filteredEquationsHtml]
</ul>
</details>
]
else
pure #[
<details>
<summary>Equations</summary>
<ul «class»="equations">
[filteredEquationsHtml]
</ul>
</details>
]

View File

@ -45,6 +45,23 @@ def toString (html : Html) : String :=
instance : ToString Html :=
⟨toString⟩
partial def textLength : Html → Nat
| text s => s.length
| element _ _ _ children =>
let lengths := children.map textLength
lengths.foldl Nat.add 0
def escapePairs : Array (String × String) :=
#[
("&", "&amp"),
("<", "&lt"),
(">", "&gt"),
("\"", "&quot")
]
def escape (s : String) : String :=
escapePairs.foldl (λ acc (o, r) => acc.replace o r) s
end Html
namespace Jsx