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
  • [←infoFormatToHtml c]
  • def equationsToHtml (i : DefinitionInfo) : HtmlM (Array Html) := do if let some eqs := i.equations then let equationsHtml ← eqs.mapM equationToHtml - pure #[ -
    - Equations - -
    - ] + let filteredEquationsHtml := equationsHtml.filter (λ eq => eq.textLength < equationLimit) + if equationsHtml.size ≠ filteredEquationsHtml.size then + pure #[ +
    + Equations + +
    + ] + else + pure #[ +
    + Equations + +
    + ] 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) := + #[ + ("&", "&"), + ("<", "<"), + (">", ">"), + ("\"", """) + ] + +def escape (s : String) : String := + escapePairs.foldl (λ acc (o, r) => acc.replace o r) s + end Html namespace Jsx