fix: show trace timings in infoview (#3985)

A regression introduced by #3801
leanprover · Apr 24, 2024 · b8a73d4 · b8a73d4
1 parent f9f2782
commit b8a73d4
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/src/Lean/Widget/InteractiveDiagnostic.lean b/src/Lean/Widget/InteractiveDiagnostic.lean
@@ -144,7 +144,9 @@ where
   | ctx,       compose d₁ d₂            => do let d₁ ← go nCtx ctx d₁; let d₂ ← go nCtx ctx d₂; pure $ d₁ ++ d₂
   | ctx,       group d                  => Format.group <$> go nCtx ctx d
   | ctx,       .trace data header children => do
-    let header := (← go nCtx ctx header).nest 4
+    let mut header := (← go nCtx ctx header).nest 4
+    if data.startTime != 0 then
+      header := f!"[{data.stopTime - data.startTime}] {header}"
     let nodes ←
       if data.collapsed && !children.isEmpty then
         let children := children.map fun child =>