fix: #113

DocGen4/Output/DocString.lean

@@ -78,7 +78,7 @@ def nameToLink? (s : String) : HtmlM (Option String) := do
     else
       match (← getCurrentName) with
       | some currentName =>
-        match res.moduleInfo.find! currentName |>.members |> filterMapDocInfo |>.find? (sameEnd ·.getName name) with
+        match res.moduleInfo.find! currentName |>.members |> filterDocInfo |>.find? (sameEnd ·.getName name) with
         | some info =>
           declNameToLink info.getName
         | _ => return none

DocGen4/Output/Module.lean

@@ -205,8 +205,9 @@ def internalNav (members : Array Name) (moduleName : Name) : HtmlM Html := do
 The main entry point to rendering the HTML for an entire module.
 -/
 def moduleToHtml (module : Process.Module) : HtmlM Html := withTheReader SiteBaseContext (setCurrentName module.name) do
-  let memberDocs ← module.members.mapM (moduleMemberToHtml module.name ·)
+  let relevantMembers := module.members.filter Process.ModuleMember.shouldRender
-  let memberNames := filterMapDocInfo module.members |>.map DocInfo.getName
+  let memberDocs ← relevantMembers.mapM (moduleMemberToHtml module.name)
+  let memberNames := filterDocInfo relevantMembers |>.map DocInfo.getName
   templateLiftExtends (baseHtmlGenerator module.name.toString) <| pure #[
     ← internalNav memberNames module.name,
     Html.element "main" false #[] memberDocs

DocGen4/Output/ToJson.lean

@@ -86,7 +86,7 @@ def DocInfo.toJson (module : Name) (info : Process.DocInfo) : HtmlM JsonDeclarat
 def Process.Module.toJson (module : Process.Module) : HtmlM Json := do
     let mut jsonDecls := []
     let mut instances := #[]
-    let declInfo := Process.filterMapDocInfo module.members
+    let declInfo := Process.filterDocInfo module.members
     for decl in declInfo do
       jsonDecls := (← DocInfo.toJson module.name decl) :: jsonDecls
       if let .instanceInfo i := decl then

DocGen4/Process/Analyze.lean

@@ -77,6 +77,10 @@ def getDocString : ModuleMember → Option String
 | docInfo i => i.getDocString
 | modDoc i => i.doc
 
+def shouldRender : ModuleMember → Bool
+| docInfo i => i.shouldRender
+| modDoc _ => true
+
 end ModuleMember
 
 inductive AnalyzeTask where
@@ -144,7 +148,7 @@ def process (task : AnalyzeTask) : MetaM (AnalyzerResult × Hierarchy) := do
   }
   return (analysis, hierarchy)
 
-def filterMapDocInfo (ms : Array ModuleMember) : Array DocInfo :=
+def filterDocInfo (ms : Array ModuleMember) : Array DocInfo :=
   ms.filterMap filter
   where
     filter : ModuleMember → Option DocInfo

DocGen4/Process/Base.lean

@@ -60,6 +60,10 @@ structure Info extends NameInfo where
   A list of (known) attributes that are attached to the declaration.
   -/
   attrs : Array String
+  /--
+  Whether this info item should be rendered
+  -/
+  render : Bool := true
   deriving Inhabited
 
 /--
@@ -147,6 +151,12 @@ Information about a `class inductive` declaration.
 -/
 abbrev ClassInductiveInfo := InductiveInfo
 
+
+/--
+Information about a constructor of an inductive type
+-/
+abbrev ConstructorInfo := Info
+
 /--
 A general type for informations about declarations.
 -/
@@ -160,6 +170,7 @@ inductive DocInfo where
 | structureInfo (info : StructureInfo) : DocInfo
 | classInfo (info : ClassInfo) : DocInfo
 | classInductiveInfo (info : ClassInductiveInfo) : DocInfo
+| ctorInfo (info : ConstructorInfo) : DocInfo
   deriving Inhabited
 
 /--

DocGen4/Process/DocInfo.lean

@@ -31,6 +31,7 @@ def getDeclarationRange : DocInfo → DeclarationRange
 | structureInfo i => i.declarationRange
 | classInfo i => i.declarationRange
 | classInductiveInfo i => i.declarationRange
+| ctorInfo i => i.declarationRange
 
 def getName : DocInfo → Name
 | axiomInfo i => i.name
@@ -42,6 +43,7 @@ def getName : DocInfo → Name
 | structureInfo i => i.name
 | classInfo i => i.name
 | classInductiveInfo i => i.name
+| ctorInfo i => i.name
 
 def getKind : DocInfo → String
 | axiomInfo _ => "axiom"
@@ -53,6 +55,7 @@ def getKind : DocInfo → String
 | structureInfo _ => "structure"
 | classInfo _ => "class"
 | classInductiveInfo _ => "class"
+| ctorInfo _ => "ctor" -- TODO: kind ctor support in js
 
 def getType : DocInfo → CodeWithInfos
 | axiomInfo i => i.type
@@ -64,6 +67,7 @@ def getType : DocInfo → CodeWithInfos
 | structureInfo i => i.type
 | classInfo i => i.type
 | classInductiveInfo i => i.type
+| ctorInfo i => i.type
 
 def getArgs : DocInfo → Array Arg
 | axiomInfo i => i.args
@@ -75,6 +79,7 @@ def getArgs : DocInfo → Array Arg
 | structureInfo i => i.args
 | classInfo i => i.args
 | classInductiveInfo i => i.args
+| ctorInfo i => i.args
 
 def getAttrs : DocInfo → Array String
 | axiomInfo i => i.attrs
@@ -86,6 +91,7 @@ def getAttrs : DocInfo → Array String
 | structureInfo i => i.attrs
 | classInfo i => i.attrs
 | classInductiveInfo i => i.attrs
+| ctorInfo i => i.attrs
 
 def getDocString : DocInfo → Option String
 | axiomInfo i => i.doc
@@ -97,6 +103,19 @@ def getDocString : DocInfo → Option String
 | structureInfo i => i.doc
 | classInfo i => i.doc
 | classInductiveInfo i => i.doc
+| ctorInfo i => i.doc
+
+def shouldRender : DocInfo → Bool
+| axiomInfo i => i.render
+| theoremInfo i => i.render
+| opaqueInfo i => i.render
+| definitionInfo i => i.render
+| instanceInfo i => i.render
+| inductiveInfo i => i.render
+| structureInfo i => i.render
+| classInfo i => i.render
+| classInductiveInfo i => i.render
+| ctorInfo i => i.render
 
 def isBlackListed (declName : Name) : MetaM Bool := do
   match ← findDeclarationRanges? declName with
@@ -135,7 +154,8 @@ def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := fun (name,
   | ConstantInfo.opaqueInfo i => return some <| opaqueInfo (← OpaqueInfo.ofOpaqueVal i)
   | ConstantInfo.defnInfo i =>
     if ← isProjFn i.name then
-      return none
+      let info ← DefinitionInfo.ofDefinitionVal i
+      return some <| definitionInfo { info with render := false }
     else
       if ← isInstance i.name then
         let info ← InstanceInfo.ofDefinitionVal i
@@ -155,8 +175,11 @@ def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := fun (name,
         return some <| classInductiveInfo (← ClassInductiveInfo.ofInductiveVal i)
       else
         return some <| inductiveInfo (← InductiveInfo.ofInductiveVal i)
+  | ConstantInfo.ctorInfo i =>
+    let info ← Info.ofConstantVal i.toConstantVal
+    return some <| ctorInfo { info with render := false }
   -- we ignore these for now
-  | ConstantInfo.ctorInfo _ | ConstantInfo.recInfo _ | ConstantInfo.quotInfo _ => return none
+  | ConstantInfo.recInfo _ | ConstantInfo.quotInfo _ => return none
 
 def getKindDescription : DocInfo → String
 | axiomInfo i => if i.isUnsafe then "unsafe axiom" else "axiom"
@@ -191,6 +214,7 @@ def getKindDescription : DocInfo → String
 | structureInfo _ => "structure"
 | classInfo _ => "class"
 | classInductiveInfo _ => "class inductive"
+| ctorInfo _ => "constructor"
 
 end DocInfo