From d5eb9f340068f3bb319bc2c7b7ef7a66ed1ca0e2 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Sun, 7 Aug 2022 17:34:41 +0200
Subject: [PATCH] chore: improve check traces

---
 src/Lean/Meta/Check.lean | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean
index 47582e0850..ea05f613ae 100644
--- a/src/Lean/Meta/Check.lean
+++ b/src/Lean/Meta/Check.lean
@@ -187,8 +187,13 @@ where
 Throw an exception if `e` is not type correct.
 -/
 def check (e : Expr) : MetaM Unit :=
-  traceCtx `Meta.check do
-    withTransparency TransparencyMode.all $ checkAux e
+  withTraceNode `Meta.check (fun res =>
+      return m!"{if res.isOk then checkEmoji else crossEmoji} {e}") do
+    try
+      withTransparency TransparencyMode.all $ checkAux e
+    catch ex =>
+      trace[Meta.check] ex.toMessageData
+      throw ex
 
 /--
 Return true if `e` is type correct.
@@ -197,12 +202,10 @@ def isTypeCorrect (e : Expr) : MetaM Bool := do
   try
     check e
     pure true
-  catch ex =>
-    trace[Meta.typeError] ex.toMessageData
+  catch _ =>
     pure false
 
 builtin_initialize
   registerTraceClass `Meta.check
-  registerTraceClass `Meta.typeError
 
 end Lean.Meta