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

@@ -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