diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean
index c66fa4f..66f5015 100644
--- a/DocGen4/Output/DocString.lean
+++ b/DocGen4/Output/DocString.lean
@@ -9,6 +9,8 @@ namespace Output
open Xml Parser Lean Parsec
+instance : Inhabited Element := ⟨"", Std.RBMap.empty, #[]⟩
+
def manyDocument : Parsec (Array Element) := many (prolog *> element <* many Misc) <* eof
partial def elementToPlainText : Xml.Element → String
@@ -28,50 +30,91 @@ def textToIdAttribute (s : String) : String :=
|>.toLower
|>.replace " " "-"
-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
- |>.insert "class" "hover-link"
- |>.insert "href" s!"#{id}"
- let anchor := Element.Element "a" anchorAttributes #[Content.Character "#"]
- let newAttrs := attrs
- |>.insert "id" id
- |>.insert "class" "markdown-heading"
- let newContents := (←
- contents.mapM (λ c => match c with
- | Content.Element e => (addAttributes e).map (Content.Element)
- | _ => pure c))
- |>.push (Content.Element anchor)
- 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
+def possibleNameToLink (s : String) : HtmlM (Option String) := do
+ let res ← getResult
+ let name := s.splitOn "." |>.foldl (λ acc part => Name.mkStr acc part) Name.anonymous
+ if res.name2ModIdx.contains name then
+ declNameToLink name
else
- let newContents ← contents.mapM λ c => match c with
- | Content.Element e => (addAttributes e).map Content.Element
- | _ => pure c
- pure ⟨ name, attrs, newContents ⟩
+ match (← getCurrentName) with
+ | some currentName =>
+ match (res.moduleInfo.find! currentName).members.find? (·.getName.toString.endsWith s) with
+ | some info =>
+ declNameToLink info.getName
+ | _ => pure none
+ | _ => pure none
+
+def extendRelativeLink (s : String) : HtmlM String := do
+ -- for relative doc links
+ if s.startsWith "#" then
+ if let some link ← possibleNameToLink (s.drop 1) then
+ pure link
+ else
+ pure s
+ -- for absolute and relative urls
+ else if s.startsWith "http" then
+ pure s
+ else pure ((←getRoot) ++ s)
+
+def possibleNameToAnchor (s : String) : HtmlM Content := do
+ let link? ← possibleNameToLink s
+ match link? with
+ | some link =>
+ let res ← getResult
+ let attributes := Std.RBMap.empty.insert "href" link
+ pure $ Content.Element $ Element.Element "a" attributes #[Content.Character s]
+ | none => pure $ Content.Character s
+
+partial def modifyElement (element : Element) (linkCode : Bool := true) : HtmlM Element :=
+ match element with
+ | 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
+ |>.insert "class" "hover-link"
+ |>.insert "href" s!"#{id}"
+ let anchor := Element.Element "a" anchorAttributes #[Content.Character "#"]
+ let newAttrs := attrs
+ |>.insert "id" id
+ |>.insert "class" "markdown-heading"
+ let newContents := (←
+ contents.mapM (λ c => match c with
+ | Content.Element e => (modifyElement e).map (Content.Element)
+ | _ => pure c))
+ |>.push (Content.Character " ")
+ |>.push (Content.Element anchor)
+ pure ⟨ name, newAttrs, newContents⟩
+ -- extend relative href for
+ else if name = "a" then
+ let root ← getRoot
+ let newAttrs ← match (attrs.find? "href").map (extendRelativeLink) with
+ | some href => href.map (attrs.insert "href")
+ | none => pure attrs
+ pure ⟨ name, newAttrs, contents⟩
+ -- auto link for inline
+ else if name = "code" then
+ let mut newContents := #[]
+ for c in contents do
+ match c with
+ | Content.Character s =>
+ newContents := newContents ++ (← s.splitOn.mapM possibleNameToAnchor)
+ | _ => newContents := newContents.push c
+ pure ⟨ name, attrs, newContents⟩
+ -- recursively modify
+ else
+ let newContents ← contents.mapM λ c => match c with
+ -- disable auto link for code blocks
+ | Content.Element e => (modifyElement e (name ≠ "pre")).map Content.Element
+ | _ => pure c
+ pure ⟨ name, attrs, newContents ⟩
def docStringToHtml (s : String) : HtmlM (Array Html) := do
let rendered := CMark.renderHtml s
match manyDocument rendered.mkIterator with
| Parsec.ParseResult.success _ res =>
res.mapM λ x => do
- pure (Html.text $ toString (← addAttributes x))
+ pure (Html.text $ toString (← modifyElement x))
| _ => pure #[Html.text rendered]
end Output