Update Trace.lean

Update src/Lean/Util/Trace.lean
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
2026-03-20 11:54:07 +00:00 · 2023-07-27 15:27:56 -07:00 · 2023-07-27 15:27:24 -07:00 · 2023-07-27 12:36:56 -07:00
1 changed files with 1 additions and 1 deletions
--- a/src/Lean/Util/Trace.lean
+++ b/src/Lean/Util/Trace.lean
@@ -193,7 +193,7 @@ def withTraceNode [MonadExcept ε m] [MonadLiftT BaseIO m] (cls : Name) (msg : E
    modifyTraces (oldTraces ++ ·)
    return (← MonadExcept.ofExcept res)
  let ref ← getRef
-  let mut m ← msg res
+  let mut m ← try msg res catch _ => pure m!"<exception thrown while producing trace node message>"
  if profiler.get opts || aboveThresh then
    m := m!"[{secs}s] {m}"
  addTraceNode oldTraces cls ref m collapsed
Author	SHA1	Message	Date
Wojciech Nawrocki	f1f693fcd5	Update Trace.lean	2023-07-27 15:27:56 -07:00
Wojciech Nawrocki	a75fc1d756	Update src/Lean/Util/Trace.lean Co-authored-by: Gabriel Ebner <gebner@gebner.org>	2023-07-27 15:27:24 -07:00
Wojciech Nawrocki	b4f08799fb	fix: handle error in withTrace message action	2023-07-27 12:36:56 -07:00