diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
index 6e8b5537b3..4ccc56c36d 100644
--- a/src/Lean/Message.lean
+++ b/src/Lean/Message.lean
@@ -244,8 +244,8 @@ partial def formatAux : NamingContext → Option MessageDataContext → MessageD
       | panic! s!"MessageData.ofLazy: expected MessageData in Dynamic, got {dyn.typeName}"
     formatAux nCtx ctx? msg
 
-protected def format (msgData : MessageData) : IO Format :=
-  formatAux { currNamespace := Name.anonymous, openDecls := [] } none msgData
+protected def format (msgData : MessageData) (ctx? : Option MessageDataContext := none) : IO Format :=
+  formatAux { currNamespace := Name.anonymous, openDecls := [] } ctx? msgData
 
 protected def toString (msgData : MessageData) : IO String := do
   return toString (← msgData.format)
diff --git a/src/Lean/Util/Profiler.lean b/src/Lean/Util/Profiler.lean
index 4be018e77a..3da0c31678 100644
--- a/src/Lean/Util/Profiler.lean
+++ b/src/Lean/Util/Profiler.lean
@@ -147,9 +147,9 @@ private partial def getFirstStart? : MessageData → Option Float
 
 private partial def addTrace (pp : Bool) (thread : ThreadWithMaps) (trace : MessageData) :
     IO ThreadWithMaps :=
-  (·.2) <$> StateT.run (go none trace) thread
+  (·.2) <$> StateT.run (go none none trace) thread
 where
-  go parentStackIdx? : _ → StateT ThreadWithMaps IO Unit
+  go parentStackIdx? ctx? : _ → StateT ThreadWithMaps IO Unit
     | .trace data msg children => do
       if data.startTime == 0 then
         return  -- no time data, skip
@@ -157,7 +157,7 @@ where
       if !data.tag.isEmpty then
         funcName := s!"{funcName}: {data.tag}"
       if pp then
-        funcName := s!"{funcName}: {← msg.format}"
+        funcName := s!"{funcName}: {← msg.format ctx?}"
       let strIdx ← modifyGet fun thread =>
         if let some idx := thread.stringMap[funcName]? then
           (idx, thread)
@@ -212,7 +212,7 @@ where
             threadCPUDelta := thread.samples.threadCPUDelta.push 0.0 |>.push (nextStart - thread.lastTime)
             length := thread.samples.length + 2
           } }
-          go (some stackIdx) c
+          go (some stackIdx) ctx? c
       -- add remaining slice after last child
       modify fun thread => { thread with
         lastTime := data.stopTime
@@ -223,7 +223,7 @@ where
           threadCPUDelta := thread.samples.threadCPUDelta.push 0.0 |>.push (data.stopTime - thread.lastTime)
           length := thread.samples.length + 2
         } }
-    | .withContext _ msg => go parentStackIdx? msg
+    | .withContext ctx msg => go parentStackIdx? (some ctx) msg
     | _ => return
 
 def Thread.new (name : String) : Thread := {