From f6622b3120eef1ee0bf9b2d98c21880237b9fbef Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 16 Jan 2020 19:32:58 -0800 Subject: [PATCH] fix: display goal at error --- src/Init/Lean/Meta/Exception.lean | 4 +--- src/Init/Lean/Meta/Message.lean | 4 +++- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Init/Lean/Meta/Exception.lean b/src/Init/Lean/Meta/Exception.lean index 6b8ae87653..715be79fb7 100644 --- a/src/Init/Lean/Meta/Exception.lean +++ b/src/Init/Lean/Meta/Exception.lean @@ -92,9 +92,7 @@ def toTraceMessageData : Exception → MessageData | notInstance i ctx => mkCtx ctx $ `notInstance ++ " " ++ i | appBuilder op msg args ctx => mkCtx ctx $ `appBuilder ++ " " ++ op ++ " " ++ args ++ " " ++ msg | synthInstance inst ctx => mkCtx ctx $ `synthInstance ++ " " ++ inst -| tactic tacName mvarId msg ctx => - mkCtx ctx $ `tacticFailure ++ " " ++ tacName ++ " " ++ msg ++ Format.line ++ - ppGoal ctx.env ctx.mctx ctx.lctx ctx.opts mvarId +| tactic tacName mvarId msg ctx => mkCtx ctx $ `tacticFailure ++ " " ++ tacName ++ " " ++ msg | bug _ _ => "internal bug" -- TODO improve | other s => s diff --git a/src/Init/Lean/Meta/Message.lean b/src/Init/Lean/Meta/Message.lean index c13fa2005f..bab1b7d986 100644 --- a/src/Init/Lean/Meta/Message.lean +++ b/src/Init/Lean/Meta/Message.lean @@ -78,7 +78,9 @@ def toMessageData : Exception → MessageData | notInstance i ctx => mkCtx ctx $ "not a type class instance " ++ i | appBuilder op msg args ctx => mkCtx ctx $ "application builder failure " ++ op ++ " " ++ args ++ " " ++ msg | synthInstance inst ctx => mkCtx ctx $ "failed to synthesize" ++ indentExpr inst -| tactic tacName mvarId msg ctx => "tactic '" ++ tacName ++ "' failed " ++ msg +| tactic tacName mvarId msg ctx => + "tactic '" ++ tacName ++ "' failed " ++ msg ++ Format.line ++ + ppGoal ctx.env ctx.mctx ctx.lctx ctx.opts mvarId | bug _ _ => "internal bug" -- TODO improve | other s => s