From 1729f4aa71cc41b74c610fb42709e28bc2e1cbfa Mon Sep 17 00:00:00 2001
From: Xubai Wang <self@xubai.wang>
Date: Thu, 17 Feb 2022 15:26:17 +0800
Subject: [PATCH] fix: fix docstring heading id

---
 DocGen4/Output/DocString.lean | 24 +++++++++++++++++++-----
 1 file changed, 19 insertions(+), 5 deletions(-)

diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean
index 0bf6683..98b2a2c 100644
--- a/DocGen4/Output/DocString.lean
+++ b/DocGen4/Output/DocString.lean
@@ -11,14 +11,28 @@ open Xml Parser Lean Parsec
 
 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) => 
+  "".intercalate (contents.toList.map contentToPlainText)
+  where
+    contentToPlainText c := match c with
+    | 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
+  |>.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 := "".intercalate (contents.map toString).toList 
-      |>.dropWhile (λ c => !(c.isAlphanum ∨ c = '-'))
-      |>.toLower
-      |>.replace " " "-"
+    let id := textToIdAttribute (elementToPlainText el)
     let anchorAttributes := Std.RBMap.empty
       |>.insert "class" "hover-link"
       |>.insert "href" s!"#{id}"