max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: include macroStack and use getBetterRef when reporting IO errors

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-15 15:13:38 -08:00
parent 8963090142
commit ef4f50d6d5
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Init/Lean/Elab/Command.lean
View file

@ -56,7 +56,8 @@ def mkMessageAux (ctx : Context) (ref : Syntax) (msgData : MessageData) (severit
mkMessageCore ctx.fileName ctx.fileMap msgData severity (ref.getPos.getD ctx.cmdPos)
private def ioErrorToMessage (ctx : Context) (ref : Syntax) (err : IO.Error) : Message :=
mkMessageAux ctx ref (toString err) MessageSeverity.error
let ref := getBetterRef ref ctx.macroStack;
mkMessageAux ctx ref (addMacroStack (toString err) ctx.macroStack) MessageSeverity.error
@[inline] def liftIOCore {α} (ctx : Context) (ref : Syntax) (x : IO α) : EIO Exception α :=
EIO.adaptExcept (fun ex => Exception.error $ ioErrorToMessage ctx ref ex) x