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

[ docs ] Show constructor for records (REPL and HTML)

Browse Source
This commit is contained in:
Johann Rudloff 2021-05-05 22:43:10 +02:00 committed by G. Allais
parent 190932fd01
commit d8891bf7b9
1 changed files with 5 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
src/Idris/DocString.idr
View File

@ -149,13 +149,15 @@ getDocsForName fc n
getDConDoc con
= do defs <- get Ctxt
Just def <- lookupCtxtExact con (gamma defs)
-- should never happen, since we know that the DCon exists:
| Nothing => pure Empty
syn <- get Syn
let [(n, str)] = lookupName con (docstrings syn)
| _ => pure Empty
ty <- resugar [] =<< normaliseHoles defs [] (type def)
let conWithTypeDoc = annotate (Decl con) (hsep [dCon (prettyName con), colon, prettyTerm ty])
let [(n, str)] = lookupName con (docstrings syn)
| _ => pure conWithTypeDoc
pure $ vcat
[ annotate (Decl con) (hsep [dCon (prettyName n), colon, prettyTerm ty])
[ conWithTypeDoc
, annotate DocStringBody $ vcat $ reflowDoc str
]