fix: #check_failure

leanprover · Feb 11, 2021 · 10bcd0b · 10bcd0b
1 parent a74960a
commit 10bcd0b
Showing 1 changed file with 5 additions and 3 deletions.
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
@@ -597,14 +597,16 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
       hasNoErrorMessages
     catch
       | ex@(Exception.error _ _) => do logException ex; pure false
-      | Exception.internal id _  => do logError "internal"; pure false -- TODO: improve `logError "internal"`
+      | Exception.internal id _  => do logError (← id.getName); pure false
     finally
       restoreMessages prevMessages
   if succeeded then
     throwError "unexpected success"
 
-@[builtinCommandElab «check_failure»] def elabCheckFailure : CommandElab := fun stx =>
-  failIfSucceeds <| elabCheck stx
+@[builtinCommandElab «check_failure»] def elabCheckFailure : CommandElab
+  | `(#check_failure $term) => do
+    failIfSucceeds <| elabCheck (← `(#check $term))
+  | _ => throwUnsupportedSyntax
 
 unsafe def elabEvalUnsafe : CommandElab
   | `(#eval%$tk $term) => do