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

[ docs ] Fix HTML formatting for record projections

Browse Source 
The `Decl` annotation should go directly on the name-type part. This
automatically fixes the `Decl` annotation being skipped, when no
docstring is found.
This commit is contained in:
Johann Rudloff 2021-06-30 18:56:51 +02:00 committed by G. Allais
parent 6fbba94c21
commit f2f83bd531
1 changed files with 2 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -244,11 +244,10 @@ getDocsForName fc n
| Nothing => pure Empty
ty <- resugar [] =<< normaliseHoles defs [] (type def)
let prettyName = pretty (nameRoot nm)
let projDecl = hsep [ fun nm prettyName, colon, prettyTerm ty ]
let projDecl = annotate (Decl nm) $ hsep [ fun nm prettyName, colon, prettyTerm ty ]
let [(_, str)] = lookupName nm (docstrings syn)
| _ => pure projDecl
pure $ annotate (Decl nm)
$ vcat [ projDecl
pure $ vcat [ projDecl
, annotate DocStringBody $ vcat (reflowDoc str)
]