Merge pull request #71 from leanprover/inductive-docstring

feat: Inductive constructor doc strings
main
Henrik Böving 2022-07-21 20:29:55 +02:00 committed by GitHub
commit f0a1ec2835
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 20 additions and 16 deletions

View File

@ -7,10 +7,21 @@ namespace Output
open scoped DocGen4.Jsx open scoped DocGen4.Jsx
def ctorToHtml (i : Process.NameInfo) : HtmlM Html := do def ctorToHtml (c : Process.NameInfo) : HtmlM Html := do
let shortName := i.name.components'.head!.toString let shortName := c.name.components'.head!.toString
let name := i.name.toString let name := c.name.toString
pure <li class="constructor" id={name}>{shortName} : [←infoFormatToHtml i.type]</li> if let some doc := c.doc then
let renderedDoc ← docStringToHtml doc
pure
<li class="constructor" id={name}>
<div class="inductive_ctor_doc">[renderedDoc]</div>
{shortName} : [←infoFormatToHtml c.type]
</li>
else
pure
<li class="constructor" id={name}>
{shortName} : [←infoFormatToHtml c.type]
</li>
def inductiveToHtml (i : Process.InductiveInfo) : HtmlM (Array Html) := do def inductiveToHtml (i : Process.InductiveInfo) : HtmlM (Array Html) := do
let constructorsHtml := <ul class="constructors">[← i.ctors.toArray.mapM ctorToHtml]</ul> let constructorsHtml := <ul class="constructors">[← i.ctors.toArray.mapM ctorToHtml]</ul>

View File

@ -20,18 +20,6 @@ def getTopLevelModules (p : Parsed) : IO (List String) := do
throw $ IO.userError "No topLevelModules provided." throw $ IO.userError "No topLevelModules provided."
pure topLevelModules pure topLevelModules
def runInitCmd (p : Parsed) : IO UInt32 := do
let topLevelModules ← getTopLevelModules p
let res ← lakeSetup topLevelModules
match res with
| Except.ok _ =>
let modules := topLevelModules.map Name.mkSimple
let hierarchy ← loadInit modules
let baseConfig := getSimpleBaseContext hierarchy
htmlOutputSetup baseConfig
pure 0
| Except.error rc => pure rc
def runSingleCmd (p : Parsed) : IO UInt32 := do def runSingleCmd (p : Parsed) : IO UInt32 := do
let topLevelModules ← getTopLevelModules p let topLevelModules ← getTopLevelModules p
let relevantModules := [p.positionalArg! "module" |>.as! String] let relevantModules := [p.positionalArg! "module" |>.as! String]

View File

@ -491,6 +491,11 @@ pre code { padding: 0 0; }
margin-left: 2ex; margin-left: 2ex;
} }
.inductive_ctor_doc {
text-indent: 2ex;
padding-top: 1ex;
}
.structure_field_doc { .structure_field_doc {
text-indent: 0; text-indent: 0;
padding-top: 1ex; padding-top: 1ex;