From d3ce268d6391d8cff2d7c6a174f7662e735972f8 Mon Sep 17 00:00:00 2001
From: Xubai Wang <self@xubai.wang>
Date: Wed, 16 Feb 2022 02:19:40 +0800
Subject: [PATCH] feat: mod doc heading attributes

---
 DocGen4/Output/Module.lean | 33 ++++++++++++++++++++++++++++++++-
 1 file changed, 32 insertions(+), 1 deletion(-)

diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean
index c6b0d76..b218d3e 100644
--- a/DocGen4/Output/Module.lean
+++ b/DocGen4/Output/Module.lean
@@ -11,6 +11,7 @@ import DocGen4.Output.Class
 import DocGen4.Output.Definition
 import DocGen4.Output.Instance
 import DocGen4.Output.ClassInductive
+import Lean.Data.Xml.Parser
 
 namespace DocGen4
 namespace Output
@@ -102,11 +103,41 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
       </div>
     </div>
 
+open Xml in
+partial def addAttributes : Element → Element
+| (Element.Element name attrs contents) => 
+  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 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.map (λ c => match c with
+      | Content.Element e => Content.Element (addAttributes e)
+      | _ => c)
+      |>.push (Content.Element anchor)
+    ⟨ name, newAttrs, newContents⟩ 
+  else
+    let newContents := contents.map λ c => match c with
+      | Content.Element e => Content.Element (addAttributes e)
+      | _ => c
+    ⟨ name, attrs, newContents⟩ 
+
 def modDocToHtml (module : Name) (mdoc : ModuleDoc) : HtmlM Html := do
-  pure 
+  let rendered := toString
     <div «class»="mod_doc">
       {Html.text (CMark.renderHtml mdoc.doc)}
     </div>
+  let modified := match Lean.Xml.parse rendered with
+  | Except.ok parsed => toString $ addAttributes parsed
+  | _                => rendered
+  pure (Html.text modified)
 
 def moduleMemberToHtml (module : Name) (member : ModuleMember) : HtmlM Html := 
   match member with