idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-24 15:07:37 +03:00
Code Issues Projects Releases Wiki Activity

Update namespaces with aliases in output

Browse Source
This commit is contained in:
Edwin Brady 2020-07-12 12:48:48 +01:00
parent 9156084075
commit 183bac8667
2 changed files with 3 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Idris/DocString.idr
View File

@ -145,7 +145,7 @@ getDocsFor fc n
Just def <- lookupCtxtExact n (gamma defs)
| Nothing => throw (UndefinedName fc n)
ty <- normaliseHoles defs [] (type def)
let doc = show n ++ " : " ++ show !(resugar [] ty)
let doc = show !(aliasName n) ++ " : " ++ show !(resugar [] ty)
++ "\n" ++ indent str
extra <- getExtra n def
pure (doc ++ extra)

3
src/Idris/Error.idr
View File

@ -162,7 +162,8 @@ perror (AllFailed ts)
where
pAlterror : (Maybe Name, Error) -> Core String
pAlterror (Just n, err)
= pure $ "If " ++ show !(getFullName n) ++ ": " ++ !(perror err) ++ "\n"
= pure $ "If " ++ show !(aliasName !(getFullName n)) ++ ": "
++ !(perror err) ++ "\n"
pAlterror (Nothing, err)
= pure $ "Possible error:\n\t" ++ !(perror err)