diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean
index e8cb33f..1cc370d 100644
--- a/DocGen4/Output.lean
+++ b/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
diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean
index eef3186..c6b0d76 100644
--- a/DocGen4/Output/Module.lean
+++ b/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
+def modDocToHtml (module : Name) (mdoc : ModuleDoc) : HtmlM Html := do
+ pure
+
+ {Html.text (CMark.renderHtml mdoc.doc)}
+
+
+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 :=
{module.toString}
@@ -162,9 +174,9 @@ def internalNav (members : Array Name) (moduleName : Name) : HtmlM Html := do
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
]
diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean
index 17f981c..89feadb 100644
--- a/DocGen4/Process.lean
+++ b/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