diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean
index 20d032ad01..b5bbd6a8be 100644
--- a/src/Lean/Util/Trace.lean
+++ b/src/Lean/Util/Trace.lean
@@ -140,16 +140,13 @@ def addTrace (cls : Name) (msg : MessageData) : m Unit := do
     let msg ← mkMsg
     addTrace cls msg
 
-private def addTraceNodeCore (oldTraces : PersistentArray TraceElem)
-    (cls : Name) (ref : Syntax) (msg : MessageData) (collapsed : Bool) : m Unit :=
-  modifyTraces fun newTraces =>
-    oldTraces.push { ref, msg := .trace cls msg (newTraces.toArray.map (·.msg)) collapsed }
-
 private def addTraceNode (oldTraces : PersistentArray TraceElem)
     (cls : Name) (ref : Syntax) (msg : MessageData) (collapsed : Bool) : m Unit :=
   withRef ref do
+  let msg := .trace cls msg ((← getTraces).toArray.map (·.msg)) collapsed
   let msg ← addMessageContext msg
-  addTraceNodeCore oldTraces cls ref msg collapsed
+  modifyTraces fun _ =>
+    oldTraces.push { ref, msg }
 
 def withSeconds [Monad m] [MonadLiftT BaseIO m] (act : m α) : m (α × Float) := do
   let start ← IO.monoNanosNow
@@ -307,6 +304,7 @@ def withTraceNodeBefore [MonadRef m] [AddMessageContext m] [MonadOptions m]
     return (← k)
   let oldTraces ← getResetTraces
   let ref ← getRef
+  -- make sure to preserve context *before* running `k`
   let msg ← withRef ref do addMessageContext (← msg)
   let (res, secs) ← withSeconds <| observing k
   let aboveThresh := trace.profiler.get opts && secs > trace.profiler.threshold.getSecs opts
@@ -316,7 +314,7 @@ def withTraceNodeBefore [MonadRef m] [AddMessageContext m] [MonadOptions m]
   let mut msg := m!"{ExceptToEmoji.toEmoji res} {msg}"
   if profiler.get opts || aboveThresh then
     msg := m!"[{secs}s] {msg}"
-  addTraceNodeCore oldTraces cls ref msg collapsed
+  addTraceNode oldTraces cls ref msg collapsed
   MonadExcept.ofExcept res
 
 end Lean
diff --git a/src/Lean/Widget/InteractiveDiagnostic.lean b/src/Lean/Widget/InteractiveDiagnostic.lean
index 487428e33e..3b5b761a30 100644
--- a/src/Lean/Widget/InteractiveDiagnostic.lean
+++ b/src/Lean/Widget/InteractiveDiagnostic.lean
@@ -164,7 +164,7 @@ where
       let more := chopUpChildren cls blockSize children[blockSize:]
       children[:blockSize].toArray.push <|
         .trace (collapsed := true) cls
-          f!"{dbgTraceVal <| children.size - blockSize} more entries..." more
+          f!"{children.size - blockSize} more entries..." more
     else children
 
 partial def msgToInteractive (msgData : MessageData) (hasWidgets : Bool) (indent : Nat := 0) : IO (TaggedText MsgEmbed) := do