From b87c1cc1ded9d0ffb38b8aeefb222b457eaf52ab Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Sun, 20 Feb 2022 13:45:18 +0100
Subject: [PATCH 1/2] 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.
---
 DocGen4/Output/Base.lean       |  4 ++--
 DocGen4/Output/Definition.lean | 31 +++++++++++++++++++++++--------
 DocGen4/ToHtmlFormat.lean      | 17 +++++++++++++++++
 3 files changed, 42 insertions(+), 10 deletions(-)

diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean
index 4579f69..68812a8 100644
--- a/DocGen4/Output/Base.lean
+++ b/DocGen4/Output/Base.lean
@@ -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]
          | _ =>
diff --git a/DocGen4/Output/Definition.lean b/DocGen4/Output/Definition.lean
index 1152b53..66cf347 100644
--- a/DocGen4/Output/Definition.lean
+++ b/DocGen4/Output/Definition.lean
@@ -7,20 +7,35 @@ 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
-    pure #[
-      <details>
-        <summary>Equations</summary>
-        <ul «class»="equations">
-          [equationsHtml]
-        </ul>
-      </details>
-    ]
+    let filteredEquationsHtml := equationsHtml.filter (λ eq => eq.textLength < equationLimit)
+    if equationsHtml.size ≠ filteredEquationsHtml.size then
+      pure #[
+        <details>
+          <summary>Equations</summary>
+          <ul «class»="equations">
+            <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>
+      ]
   else
     pure #[]
 
diff --git a/DocGen4/ToHtmlFormat.lean b/DocGen4/ToHtmlFormat.lean
index beddf74..64e9b6a 100644
--- a/DocGen4/ToHtmlFormat.lean
+++ b/DocGen4/ToHtmlFormat.lean
@@ -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

From a86c3843546c07bc85b3ddd730805010a8bcf3f2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Sun, 20 Feb 2022 13:52:57 +0100
Subject: [PATCH 2/2] fix: Readd equations for instances

---
 DocGen4/Output/Module.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean
index 942051b..a703ccf 100644
--- a/DocGen4/Output/Module.lean
+++ b/DocGen4/Output/Module.lean
@@ -89,6 +89,7 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
   let extraInfoHtml ← match doc with
   | DocInfo.classInfo i => pure #[←classInstancesToHtml i.instances]
   | DocInfo.definitionInfo i => equationsToHtml i
+  | DocInfo.instanceInfo i => equationsToHtml i
   | DocInfo.classInductiveInfo i => pure #[←classInstancesToHtml i.instances]
   | i => pure #[]
   let attrs := doc.getAttrs