From 385a38a0036ef54f54e8f0cd7ff74ca404fe8392 Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Wed, 16 Feb 2022 01:06:46 +0800 Subject: [PATCH] feat: basic mod doc without attributes --- DocGen4/Output.lean | 2 +- DocGen4/Output/Module.lean | 16 +++++++++++-- DocGen4/Process.lean | 49 ++++++++++++++++++++++++++++---------- 3 files changed, 51 insertions(+), 16 deletions(-) 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