feat: basic mod doc without attributes

DocGen4/Output.lean

@@ -71,7 +71,7 @@ def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do
 
   let mut declList := #[]
   for (_, mod) in result.moduleInfo.toArray do
-    for decl in mod.members do
+    for decl in mod.members.filter ModuleMember.isDocInfo do
       let findHtml := ReaderT.run (findRedirectHtml decl.getName) config
       let findDir := basePath / "find" / decl.getName.toString
       FS.createDirAll findDir

DocGen4/Output/Module.lean

@@ -3,6 +3,7 @@ Copyright (c) 2021 Henrik Böving. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+import CMark
 import DocGen4.Output.Template
 import DocGen4.Output.Inductive
 import DocGen4.Output.Structure
@@ -101,6 +102,17 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
       </div>
     </div>
 
+def modDocToHtml (module : Name) (mdoc : ModuleDoc) : HtmlM Html := do
+  pure 
+    <div «class»="mod_doc">
+      {Html.text (CMark.renderHtml mdoc.doc)}
+    </div>
+
+def moduleMemberToHtml (module : Name) (member : ModuleMember) : HtmlM Html := 
+  match member with
+  | ModuleMember.docInfo d => docInfoToHtml module d
+  | ModuleMember.modDoc d => modDocToHtml module d
+
 def declarationToNavLink (module : Name) : Html :=
   <div «class»="nav_link">
     <a «class»="break_within" href={s!"#{module.toString}"}>{module.toString}</a>
@@ -162,9 +174,9 @@ def internalNav (members : Array Name) (moduleName : Name) : HtmlM Html := do
     </nav>
 
 def moduleToHtml (module : Module) : HtmlM Html := withReader (setCurrentName module.name) do
-  let docInfos ← module.members.mapM (λ i => docInfoToHtml module.name i)
+  let docInfos ← module.members.mapM (λ i => moduleMemberToHtml module.name i)
   templateExtends (baseHtmlArray module.name.toString) $ pure #[
-    ←internalNav (module.members.map DocInfo.getName) module.name,
+    ←internalNav (module.members.filter ModuleMember.isDocInfo |>.map ModuleMember.getName) module.name,
     Html.element "main" false #[] docInfos
   ]
 

DocGen4/Process.lean

@@ -101,16 +101,17 @@ def getDeclarationRange : DocInfo → DeclarationRange
 | classInfo i => i.declarationRange
 | classInductiveInfo i => i.declarationRange
 
-def lineOrder (l r : DocInfo) : Bool :=
-  l.getDeclarationRange.pos.line < r.getDeclarationRange.pos.line
-
 end DocInfo
 
+inductive ModuleMember where
+| docInfo (info : DocInfo) : ModuleMember
+| modDoc (doc : ModuleDoc) : ModuleMember
+deriving Inhabited
+
 structure Module where
   name : Name
-  doc : Option String
   -- Sorted according to their line numbers
-  members : Array DocInfo
+  members : Array ModuleMember
   deriving Inhabited
 
 partial def typeToArgsType (e : Expr) : (Array (Name × Expr × BinderInfo) × Expr) :=
@@ -459,6 +460,29 @@ def getDocString : DocInfo → Option String
 
 end DocInfo
 
+namespace ModuleMember
+
+def getDeclarationRange : ModuleMember → DeclarationRange
+| docInfo i => i.getDeclarationRange
+| modDoc i => i.declarationRange
+
+def order (l r : ModuleMember) : Bool :=
+  Position.lt l.getDeclarationRange.pos r.getDeclarationRange.pos
+
+def isDocInfo : ModuleMember → Bool
+| docInfo _ => true
+| _ => false
+
+def getName : ModuleMember → Name
+| docInfo i => i.getName
+| modDoc i => Name.anonymous
+
+def getDocString : ModuleMember → Option String
+| docInfo i => i.getDocString
+| modDoc i => i.doc
+
+end ModuleMember
+
 structure AnalyzerResult where
   name2ModIdx : HashMap Name ModuleIdx
   moduleNames : Array Name
@@ -472,13 +496,12 @@ def process : MetaM AnalyzerResult := do
   let env ← getEnv
   let mut res := mkHashMap env.header.moduleNames.size
   for module in env.header.moduleNames do
-    -- TODO: Check why modules can have multiple doc strings and add that later on
-    let moduleDoc := match getModuleDoc? env module with
-    | none => none
-    | some #[] => none
-    | some doc => doc.get! 0
+    let modDocs := match getModuleDoc? env module with
+    | none => #[]
+    | some ds => ds
+    |>.map (λ doc => ModuleMember.modDoc doc)
 
-    res := res.insert module (Module.mk module moduleDoc #[])
+    res := res.insert module (Module.mk module modDocs)
 
   for cinfo in env.constants.toList do
     try
@@ -487,7 +510,7 @@ def process : MetaM AnalyzerResult := do
         let some modidx := env.getModuleIdxFor? dinfo.getName | unreachable!
         let moduleName := env.allImportedModuleNames.get! modidx
         let module := res.find! moduleName
-        res := res.insert moduleName {module with members := module.members.push dinfo}
+        res := res.insert moduleName {module with members := module.members.push (ModuleMember.docInfo dinfo)}
     catch e =>
       IO.println s!"WARNING: Failed to obtain information for: {cinfo.fst}: {←e.toMessageData.toString}"
 
@@ -495,7 +518,7 @@ def process : MetaM AnalyzerResult := do
   let mut adj := Array.mkArray res.size (Array.mkArray res.size false)
   -- TODO: This could probably be faster if we did an insertion sort above instead
   for (moduleName, module) in res.toArray do
-    res := res.insert moduleName {module with members := module.members.qsort DocInfo.lineOrder}
+    res := res.insert moduleName {module with members := module.members.qsort ModuleMember.order}
     let some modIdx := env.getModuleIdx? moduleName | unreachable!
     let moduleData := env.header.moduleData.get! modIdx
     for imp in moduleData.imports do