From ef4f50d6d58fbd6ea76788733cb17d19edffb0d8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 15 Jan 2020 15:13:38 -0800 Subject: [PATCH] fix: include `macroStack` and use `getBetterRef` when reporting IO errors --- src/Init/Lean/Elab/Command.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Init/Lean/Elab/Command.lean b/src/Init/Lean/Elab/Command.lean index 4469be6fc2..440672bd32 100644 --- a/src/Init/Lean/Elab/Command.lean +++ b/src/Init/Lean/Elab/Command.lean @@ -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