fix: fix docstring heading id
parent
5790172eab
commit
1729f4aa71
|
@ -11,14 +11,28 @@ open Xml Parser Lean Parsec
|
||||||
|
|
||||||
def manyDocument : Parsec (Array Element) := many (prolog *> element <* many Misc) <* eof
|
def manyDocument : Parsec (Array Element) := many (prolog *> element <* many Misc) <* eof
|
||||||
|
|
||||||
partial def addAttributes : Element → Element
|
partial def elementToPlainText : Xml.Element → String
|
||||||
| (Element.Element name attrs contents) =>
|
| (Element.Element name attrs contents) =>
|
||||||
-- heading only
|
"".intercalate (contents.toList.map contentToPlainText)
|
||||||
if name = "h1" ∨ name = "h2" ∨ name = "h3" ∨ name = "h4" ∨ name = "h5" ∨ name = "h6" then
|
where
|
||||||
let id := "".intercalate (contents.map toString).toList
|
contentToPlainText c := match c with
|
||||||
|>.dropWhile (λ c => !(c.isAlphanum ∨ c = '-'))
|
| Content.Element el => elementToPlainText el
|
||||||
|
| Content.Comment _ => ""
|
||||||
|
| Content.Character s => s
|
||||||
|
|
||||||
|
def dropAllCharWhile (s : String) (p : Char → Bool) : String :=
|
||||||
|
⟨ s.data.filter p ⟩
|
||||||
|
|
||||||
|
def textToIdAttribute (s : String) : String :=
|
||||||
|
dropAllCharWhile s (λ c => (c.isAlphanum ∨ c = '-' ∨ c = ' '))
|
||||||
|>.toLower
|
|>.toLower
|
||||||
|>.replace " " "-"
|
|>.replace " " "-"
|
||||||
|
|
||||||
|
partial def addAttributes : Element → Element
|
||||||
|
| el@(Element.Element name attrs contents) =>
|
||||||
|
-- heading only
|
||||||
|
if name = "h1" ∨ name = "h2" ∨ name = "h3" ∨ name = "h4" ∨ name = "h5" ∨ name = "h6" then
|
||||||
|
let id := textToIdAttribute (elementToPlainText el)
|
||||||
let anchorAttributes := Std.RBMap.empty
|
let anchorAttributes := Std.RBMap.empty
|
||||||
|>.insert "class" "hover-link"
|
|>.insert "class" "hover-link"
|
||||||
|>.insert "href" s!"#{id}"
|
|>.insert "href" s!"#{id}"
|
||||||
|
|
Loading…
Reference in New Issue