idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-24 04:09:10 +03:00
Code Issues Projects Releases Wiki Activity

[ docs ] Ignore empty record field docstrings

Browse Source
This commit is contained in:
Johann Rudloff 2021-06-30 21:01:52 +02:00 committed by G. Allais
parent 7c1ab56ca0
commit 5e70a77310
1 changed files with 7 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
src/Idris/Doc/String.idr
View File

@ -245,11 +245,13 @@ getDocsForName fc n
ty <- resugar [] =<< normaliseHoles defs [] (type def)
let prettyName = pretty (nameRoot nm)
let projDecl = annotate (Decl nm) $ hsep [ fun nm prettyName, colon, prettyTerm ty ]
let [(_, str)] = lookupName nm (docstrings syn)
| _ => pure projDecl
pure $ vcat [ projDecl
, annotate DocStringBody $ vcat (reflowDoc str)
]
case lookupName nm (docstrings syn) of
[(_, "")] => pure projDecl
[(_, str)] =>
pure $ vcat [ projDecl
, annotate DocStringBody $ vcat (reflowDoc str)
]
_ => pure projDecl
getFieldsDoc : Name -> Core (List (Doc IdrisDocAnn))
getFieldsDoc recName