From 9158899145ae7fbd2cfb0d0f97e908bfd7eb8904 Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@protonmail.com>
Date: Wed, 28 Jul 2021 20:29:56 -0700
Subject: [PATCH] feat: pp.analize try/catch and trace

---
 src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
index 24d7d8245b..e6a62547a7 100644
--- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
@@ -400,11 +400,15 @@ def topDownAnalyze (e : Expr) : MetaM OptionsPerPos := do
   traceCtx `pp.analyze do
     withReader (fun ctx => { ctx with config := Lean.Elab.Term.setElabConfig ctx.config }) do
       let ϕ : AnalyzeM OptionsPerPos := do analyze; (← get).annotations
-      ϕ { knowsType := true, knowsLevel := true } (mkRoot e) |>.run' {}
+      try ϕ { knowsType := true, knowsLevel := true } (mkRoot e) |>.run' {}
+      catch ex =>
+        trace[pp.analyze.error] "{← ex.toMessageData.toString}"
+        pure {}
 
 builtin_initialize
   registerTraceClass `pp.analyze
   registerTraceClass `pp.analyze.annotate
   registerTraceClass `pp.analyze.tryUnify
+  registerTraceClass `pp.analyze.error
 
 end Lean.PrettyPrinter.Delaborator