diff --git a/DocGen4/Output/Definition.lean b/DocGen4/Output/Definition.lean index aa0e255..374c10c 100644 --- a/DocGen4/Output/Definition.lean +++ b/DocGen4/Output/Definition.lean @@ -25,11 +25,11 @@ def equationsToHtml (i : DefinitionInfo) : HtmlM (Option Html) := do def definitionToHtml (i : DefinitionInfo) : HtmlM (Array Html) := do let equationsHtml? ← equationsToHtml i - let docstringHtml? := i.doc.map docStringToHtml + let docstringHtml? ← i.doc.mapM docStringToHtml match equationsHtml?, docstringHtml? with - | some e, some d => pure #[e, d] + | some e, some d => pure (#[e] ++ d) | some e, none => pure #[e] - | none , some e => pure #[e] + | none , some d => pure d | none , none => pure #[] diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index 98b2a2c..c66fa4f 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -28,9 +28,15 @@ def textToIdAttribute (s : String) : String := |>.toLower |>.replace " " "-" -partial def addAttributes : Element → Element -| el@(Element.Element name attrs contents) => - -- heading only +def extendRelativeLink (link : String) (root : String) : String := + -- HACK: better way to detect absolute links + if link.startsWith "http" then + link + else root ++ link + +partial def addAttributes : Element → HtmlM Element +| el@(Element.Element name attrs contents) => do + -- add id and class to if name = "h1" ∨ name = "h2" ∨ name = "h3" ∨ name = "h4" ∨ name = "h5" ∨ name = "h6" then let id := textToIdAttribute (elementToPlainText el) let anchorAttributes := Std.RBMap.empty @@ -40,24 +46,33 @@ partial def addAttributes : Element → Element let newAttrs := attrs |>.insert "id" id |>.insert "class" "markdown-heading" - let newContents := - contents.map (λ c => match c with - | Content.Element e => Content.Element (addAttributes e) - | _ => c) + let newContents := (← + contents.mapM (λ c => match c with + | Content.Element e => (addAttributes e).map (Content.Element) + | _ => pure c)) |>.push (Content.Element anchor) - ⟨ name, newAttrs, newContents⟩ + pure ⟨ name, newAttrs, newContents⟩ + -- extend relative href for + else if name = "a" then + let root ← getRoot + let newAttrs := match attrs.find? "href" with + | some href => attrs.insert "href" (extendRelativeLink href root) + | none => attrs + pure ⟨ name, newAttrs, contents⟩ + -- recursively modify else - let newContents := contents.map λ c => match c with - | Content.Element e => Content.Element (addAttributes e) - | _ => c - ⟨ name, attrs, newContents ⟩ + let newContents ← contents.mapM λ c => match c with + | Content.Element e => (addAttributes e).map Content.Element + | _ => pure c + pure ⟨ name, attrs, newContents ⟩ -def docStringToHtml (s : String) : Html := +def docStringToHtml (s : String) : HtmlM (Array Html) := do let rendered := CMark.renderHtml s - let attributed := match manyDocument rendered.mkIterator with - | Parsec.ParseResult.success _ res => "".intercalate (res.map addAttributes |>.map toString).toList - | _ => rendered - Html.text attributed + match manyDocument rendered.mkIterator with + | Parsec.ParseResult.success _ res => + res.mapM λ x => do + pure (Html.text $ toString (← addAttributes x)) + | _ => pure #[Html.text rendered] end Output end DocGen4 diff --git a/DocGen4/Output/Inductive.lean b/DocGen4/Output/Inductive.lean index 490c127..5535290 100644 --- a/DocGen4/Output/Inductive.lean +++ b/DocGen4/Output/Inductive.lean @@ -13,9 +13,9 @@ def ctorToHtml (i : NameInfo) : HtmlM Html := do def inductiveToHtml (i : InductiveInfo) : HtmlM (Array Html) := do let constructorsHtml := - let docstringHtml? := i.doc.map docStringToHtml + let docstringHtml? ← i.doc.mapM docStringToHtml match docstringHtml? with - | some d => pure #[constructorsHtml, d] + | some d => pure (#[constructorsHtml] ++ d) | none => pure #[constructorsHtml] end Output diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index 9200498..394c509 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -82,7 +82,7 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do | DocInfo.instanceInfo i => instanceToHtml i | DocInfo.classInductiveInfo i => classInductiveToHtml i | i => match i.getDocString with - | some d => pure #[docStringToHtml d] + | some d => pure (← docStringToHtml d) | _ => pure #[] let attrs := doc.getAttrs @@ -108,7 +108,7 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do def modDocToHtml (module : Name) (mdoc : ModuleDoc) : HtmlM Html := do pure
- {docStringToHtml mdoc.doc} + [←docStringToHtml mdoc.doc]
def moduleMemberToHtml (module : Name) (member : ModuleMember) : HtmlM Html := diff --git a/DocGen4/Output/Structure.lean b/DocGen4/Output/Structure.lean index abce904..ab6e4d5 100644 --- a/DocGen4/Output/Structure.lean +++ b/DocGen4/Output/Structure.lean @@ -27,9 +27,9 @@ def structureToHtml (i : StructureInfo) : HtmlM (Array Html) := do
  • )
  • ) - let docstringHtml? := i.doc.map docStringToHtml + let docstringHtml? ← i.doc.mapM docStringToHtml match docstringHtml? with - | some d => pure #[structureHtml, d] + | some d => pure (#[structureHtml] ++ d) | none => pure #[structureHtml] end Output