mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-15 22:32:19 +03:00
[ docs ] Add record field docstrings to the RF-name as well
A record field can add two names to the context, a UN-name and an RF-name. The docstring is now saved for both names, so that it can always be found when one of the names can be resolved. Previously the docstring was only saved for the UN-name which led to the docs missing when looking up the (.fieldName) version, e.g. when listing docs for the record type.
This commit is contained in:
parent
af9f72466f
commit
7c1ab56ca0
@ -770,10 +770,15 @@ mutual
|
||||
Core IField
|
||||
desugarField ps ns (MkField fc doc rig p n ty)
|
||||
= do addDocStringNS ns n doc
|
||||
addDocStringNS ns (toRF n) doc
|
||||
syn <- get Syn
|
||||
pure (MkIField fc rig !(traverse (desugar AnyExpr ps) p )
|
||||
n !(bindTypeNames fc (usingImpl syn)
|
||||
ps !(desugar AnyExpr ps ty)))
|
||||
where
|
||||
toRF : Name -> Name
|
||||
toRF (UN n) = RF n
|
||||
toRF n = n
|
||||
|
||||
export
|
||||
desugarFnOpt : {auto s : Ref Syn SyntaxInfo} ->
|
||||
|
Loading…
Reference in New Issue
Block a user