Merge pull request #36 from leanprover/better-equations

Better equations

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]
          | _ =>

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 #[
+    let filteredEquationsHtml := equationsHtml.filter (λ eq => eq.textLength < equationLimit)
-      <details>
+    if equationsHtml.size ≠ filteredEquationsHtml.size then
-        <summary>Equations</summary>
+      pure #[
-        <ul «class»="equations">
+        <details>
-          [equationsHtml]
+          <summary>Equations</summary>
-        </ul>
+          <ul «class»="equations">
-      </details>
+            <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 #[]
 

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

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