From 926a76e6b769f3f22f8ed2bb24ad82deb1e597dd Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 9 Dec 2024 09:53:22 -0600 Subject: [PATCH] fix: indent nested traces correctly Presumably this worked before due to extra `.group` nodes appearing. I think `group`s should be implied by the children of a trace node. Not tested as I do not have a working setup for the latest Lean, though there is a test case at https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/trace.20nodes.20do.20not.20nest.20correctly.20in.20the.20infoview/near/487028252. --- src/Lean/Message.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index 65fe62c274c3..0eeb8c4c0ea9 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -237,7 +237,7 @@ partial def formatAux : NamingContext → Option MessageDataContext → MessageD msg := f!"{msg} [{data.stopTime - data.startTime}]" msg := f!"{msg} {(← formatAux nCtx ctx header).nest 2}" let children ← children.mapM (formatAux nCtx ctx) - return .nest 2 (.joinSep (msg::children.toList) "\n") + return .nest 2 (.group <| .joinSep (msg::children.toList) "\n") | nCtx, ctx?, ofLazy pp _ => do let dyn ← pp (ctx?.map (mkPPContext nCtx)) let some msg := dyn.get? MessageData