refactor: docstring between basic and extra info

clean up code

DocGen4/Output/Class.lean

@@ -21,7 +21,7 @@ def classInstancesToHtml (instances : Array Name) : HtmlM Html := do
     </details>
 
 def classToHtml (i : ClassInfo) : HtmlM (Array Html) := do
-  pure $ (←structureToHtml i.toStructureInfo).push (←classInstancesToHtml i.instances)
+  pure $ (←structureToHtml i.toStructureInfo)
 
 end Output
 end DocGen4

DocGen4/Output/ClassInductive.lean

@@ -7,7 +7,7 @@ namespace DocGen4
 namespace Output
 
 def classInductiveToHtml (i : ClassInductiveInfo) : HtmlM (Array Html) := do
-  pure $ (←inductiveToHtml i.toInductiveInfo).push (←classInstancesToHtml i.instances)
+  pure $ (←inductiveToHtml i.toInductiveInfo)
 
 end Output
 end DocGen4

DocGen4/Output/Definition.lean

@@ -10,25 +10,19 @@ open Lean Widget
 def equationToHtml (c : CodeWithInfos) : HtmlM Html := do
   pure <li «class»="equation">[←infoFormatToHtml c]</li>
 
-def equationsToHtml (i : DefinitionInfo) : HtmlM (Option Html) := do
+def equationsToHtml (i : DefinitionInfo) : HtmlM (Array Html) := do
   if let some eqs := i.equations then
     let equationsHtml ← eqs.mapM equationToHtml
-    pure
+    pure #[
       <details>
         <summary>Equations</summary>
         <ul «class»="equations">
           [equationsHtml]
         </ul>
       </details>
+    ]
   else
-    pure none
+    pure #[]
-
-def definitionToHtml (i : DefinitionInfo) : HtmlM (Array Html) := do
-  let equationsHtml? ← equationsToHtml i
-  match equationsHtml? with
-  | some e => pure #[e]
-  | none   => pure #[]
-
 
 end Output
 end DocGen4

DocGen4/Output/DocString.lean

@@ -1,8 +1,9 @@
 import CMark
 import DocGen4.Output.Template
 import Lean.Data.Parsec
+import Unicode.General.GeneralCategory
 
-open Lean
+open Lean Unicode
 
 namespace DocGen4
 namespace Output
@@ -11,26 +12,44 @@ open Xml Parser Lean Parsec
 
 instance : Inhabited Element := ⟨"", Std.RBMap.empty, #[]⟩
 
+/-- Parse an array of Xml/Html document from String. -/
 def manyDocument : Parsec (Array Element) := many (prolog *> element <* many Misc) <* eof
 
-partial def elementToPlainText : Xml.Element → String
+/--
-| (Element.Element name attrs contents) => 
+  Generate id for heading elements, with the following rules:
-  "".intercalate (contents.toList.map contentToPlainText)
+
+  1. Characters in `letter`, `number` and `symbol` unicode categories are preserved.
+  2. Any sequences of Characters in `mark`, `punctuation`, `separator` and `other` categories are replaced by a single dash.
+  3. Cases (upper and lower) are preserved.
+  4. Xml/Html tags are ignored.
+-/
+partial def xmlGetHeadingId (el : Xml.Element) : String :=
+  elementToPlainText el |> replaceCharSeq unicodeToDrop "-"
   where
+    elementToPlainText el := match el with 
+    | (Element.Element name attrs contents) => 
+      "".intercalate (contents.toList.map contentToPlainText)
     contentToPlainText c := match c with
     | Content.Element el => elementToPlainText el
     | Content.Comment _ => ""
     | Content.Character s => s
+    replaceCharSeq pattern replacement s :=
+      s.split pattern
+      |>.filter (!·.isEmpty)
+      |> replacement.intercalate
+    unicodeToDrop char := 
+      charInGeneralCategory char GeneralCategory.mark ||
+      charInGeneralCategory char GeneralCategory.punctuation ||
+      charInGeneralCategory char GeneralCategory.separator ||
+      charInGeneralCategory char GeneralCategory.other  
 
-def dropAllCharWhile (s : String) (p : Char → Bool) : String :=
+/--
-  ⟨ s.data.filter p ⟩ 
+  This function try to find the given name, both globally and in current module.
 
-def textToIdAttribute (s : String) : String :=
+  For global search, a precise name is need. If the global search fails, the function
-  dropAllCharWhile s (λ c => (c.isAlphanum ∨ c = '-' ∨ c = ' '))
+  tries to find a local one that ends with the given search name.
-  |>.toLower
+-/
-  |>.replace " " "-"
+def nameToLink? (s : String) : HtmlM (Option String) := do
-
-def possibleNameToLink (s : String) : HtmlM (Option String) := do
   let res ← getResult
   let name := s.splitOn "." |>.foldl (λ acc part => Name.mkStr acc part) Name.anonymous
   -- with exactly the same name
@@ -46,10 +65,18 @@ def possibleNameToLink (s : String) : HtmlM (Option String) := do
       | _ => pure none
     | _ => pure none
 
-def extendRelativeLink (s : String)  : HtmlM String := do
+/--
+  Extend links with following rules:
+
+  1. if the link starts with `##`, a name search is used and will panic if not found
+  2. if the link starts with `#`, it's treated as id link, no modification
+  3. if the link starts with `http`, it's an absolute one, no modification
+  4. otherwise it's a relative link, extend it with base url
+-/
+def extendLink (s : String)  : HtmlM String := do
   -- for intra doc links
   if s.startsWith "##" then
-    if let some link ← possibleNameToLink (s.drop 2) then
+    if let some link ← nameToLink? (s.drop 2) then
       pure link
     else
       panic! s!"Cannot find {s.drop 2}, only full name and abbrev in current module is supported"
@@ -61,51 +88,70 @@ def extendRelativeLink (s : String)  : HtmlM String := do
     pure s
   else pure ((←getRoot) ++ s)
 
-def possibleNameToAnchor (s : String) : HtmlM Content := do
+/-- Add attributes for heading. -/
-  let link? ← possibleNameToLink s
+def addHeadingAttributes (el : Element) (modifyElement : Element → HtmlM Element) : HtmlM Element := do
-  match link? with
+  match el with
-  | some link => 
+  | Element.Element name attrs contents => do
-    let res ← getResult
+    let id := xmlGetHeadingId el
-    let attributes := Std.RBMap.empty.insert "href" link
+    let anchorAttributes := Std.RBMap.empty
-    pure $ Content.Element $ Element.Element "a" attributes #[Content.Character s]
+      |>.insert "class" "hover-link"
-  | none => pure $ Content.Character s
+      |>.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 anchor links. -/
+def extendAnchor (el : Element) : HtmlM Element := do
+  match el with
+  | Element.Element name attrs contents =>
+    let root ← getRoot
+    let newAttrs ← match (attrs.find? "href").map extendLink with
+    | some href => href.map (attrs.insert "href")
+    | none => pure attrs
+    pure ⟨ name, newAttrs, contents⟩
+
+/-- Automatically add intra documentation link for inline code span. -/
+def autoLink (el : Element) : HtmlM Element := do
+  match el with
+  | Element.Element name attrs contents =>
+    let mut newContents := #[]
+    for c in contents do
+      match c with
+      | Content.Character s =>
+        newContents := newContents ++ (← s.splitOn.mapM linkify).intersperse (Content.Character " ")
+      | _ => newContents := newContents.push c
+    pure ⟨ name, attrs, newContents ⟩
+  where
+    linkify s := do
+      let link? ← nameToLink? 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
+
+/-- Core function of modifying the cmark rendered docstring html. -/
 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 <h_></h_>
     if name = "h1" ∨ name = "h2" ∨ name = "h3" ∨ name = "h4" ∨ name = "h5" ∨ name = "h6" then
-      let id := textToIdAttribute (elementToPlainText el)
+      addHeadingAttributes el modifyElement
-      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 <a></a>
     else if name = "a" then
-      let root ← getRoot
+      extendAnchor el
-      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 <code></code>
-    else if name = "code" ∧ linkCode then
+    else if name = "code" ∧ linkCode = true then
-      let mut newContents := #[]
+      autoLink el
-      for c in contents do
-        match c with
-        | Content.Character s =>
-          newContents := newContents ++ (← s.splitOn.mapM possibleNameToAnchor).intersperse (Content.Character " ")
-        | _ => newContents := newContents.push c
-      pure ⟨ name, attrs, newContents⟩
     -- recursively modify
     else
       let newContents ← contents.mapM λ c => match c with
@@ -114,6 +160,7 @@ partial def modifyElement (element : Element) (linkCode : Bool := true) : HtmlM
         | _ => pure c
       pure ⟨ name, attrs, newContents ⟩ 
 
+/-- Convert docstring to Html. -/
 def docStringToHtml (s : String) : HtmlM (Array Html) := do
   let rendered := CMark.renderHtml s
   match manyDocument rendered.mkIterator with

DocGen4/Output/Instance.lean

@@ -4,7 +4,5 @@ import DocGen4.Output.Definition
 namespace DocGen4
 namespace Output
 
-def instanceToHtml (i : InstanceInfo) : HtmlM (Array Html) := definitionToHtml i
-
 end Output
 end DocGen4

DocGen4/Output/Module.lean

@@ -74,17 +74,23 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do
   pure <div «class»="decl_header"> [nodes] </div>
 
 def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
+  -- basic info like headers, types, structure fields, etc.
   let docInfoHtml ← match doc with
   | DocInfo.inductiveInfo i => inductiveToHtml i
   | DocInfo.structureInfo i => structureToHtml i
   | DocInfo.classInfo i => classToHtml i
-  | DocInfo.definitionInfo i => definitionToHtml i
-  | DocInfo.instanceInfo i => instanceToHtml i
   | DocInfo.classInductiveInfo i => classInductiveToHtml i
   | i => pure #[]
+  -- rendered doc stirng
   let docStringHtml ← match doc.getDocString with
   | some s => docStringToHtml s
   | none => pure #[]
+  -- extra information like equations and instances
+  let extraInfoHtml ← match doc with
+  | DocInfo.classInfo i => pure #[←classInstancesToHtml i.instances]
+  | DocInfo.definitionInfo i => equationsToHtml i
+  | DocInfo.classInductiveInfo i => pure #[←classInstancesToHtml i.instances]
+  | i => pure #[]
   let attrs := doc.getAttrs
   let attrsHtml :=
     if attrs.size > 0 then
@@ -101,8 +107,9 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
         </div>
         [attrsHtml]
         {←docInfoHeader doc}
-        [docStringHtml]
         [docInfoHtml]
+        [docStringHtml]
+        [extraInfoHtml]
       </div>
     </div>
 

lakefile.lean

@@ -7,7 +7,11 @@ package «doc-gen4» {
   dependencies := #[
     {
       name := `CMark
-      src := Source.git "https://github.com/xubaiw/CMark.lean" "0c59e4f"
+      src := Source.git "https://github.com/xubaiw/CMark.lean" "0c59e4fa0f8864502dc9e661d437be842d29d708"
+    },
+    {
+      name := `Unicode
+      src := Source.git "https://github.com/xubaiw/Unicode.lean" "88ad4aacfcc7ab941a22c54de3e4fef0809cda87"
     }
   ]
 }