From 1eff4be172e0272219587e9acff3f5e3332bdc8d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 6 Aug 2020 10:06:24 -0700 Subject: [PATCH] feat: use `Meta.Example.other` `ref : Syntax` if it contains position information --- src/Lean/Elab/Term.lean | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index f06b2c1194..307b714d0f 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -236,7 +236,14 @@ mkMessageCore ctx.fileName ctx.fileMap msgData severity (ref.getPos.getD ctx.cmd /-- Auxiliary function for `liftMetaM` -/ private def fromMetaException (ctx : Context) (ref : Syntax) (ex : Meta.Exception) : Exception := -Exception.ex $ Elab.Exception.error $ mkMessageAux ctx ref ex.toMessageData MessageSeverity.error +let mk (ref : Syntax) : Exception := + Exception.ex $ Elab.Exception.error $ mkMessageAux ctx ref ex.toMessageData MessageSeverity.error; +match ex with +| Meta.Exception.other ref' ex => + match ref'.getPos with + | some _ => mk ref' + | _ => mk ref +| _ => mk ref /-- Auxiliary function for `liftMetaM` -/ private def fromMetaState (ref : Syntax) (ctx : Context) (s : State) (newS : Meta.State) (oldTraceState : TraceState) : State :=