chore: do not display MessageData tags by default

src/Lean/Elab/Log.lean

@@ -77,7 +77,7 @@ def logException [MonadLiftT IO m] (ex : Exception) : m Unit := do
       logError m!"internal exception: {name}"
 
 def logTrace (cls : Name) (msgData : MessageData) : m Unit := do
-  logInfo (MessageData.tagged cls msgData)
+  logInfo (MessageData.tagged cls m!"[{cls}] {msgData}")
 
 @[inline] def trace [MonadOptions m] (cls : Name) (msg : Unit → MessageData) : m Unit := do
   if checkTraceOption (← getOptions) cls then

src/Lean/Message.lean

@@ -105,7 +105,7 @@ partial def formatAux : NamingContext → Option MessageDataContext → MessageD
   | nCtx, some ctx,  ofGoal mvarId            => ppGoal (mkPPContext nCtx ctx) mvarId
   | nCtx, _,         withContext ctx d        => formatAux nCtx ctx d
   | _,    ctx,       withNamingContext nCtx d => formatAux nCtx ctx d
-  | nCtx, ctx,       tagged cls d             => do let d ← formatAux nCtx ctx d; pure $ Format.sbracket (format cls) ++ " " ++ d
+  | nCtx, ctx,       tagged _ d               => formatAux nCtx ctx d
   | nCtx, ctx,       nest n d                 => Format.nest n <$> formatAux nCtx ctx d
   | nCtx, ctx,       compose d₁ d₂            => do let d₁ ← formatAux nCtx ctx d₁; let d₂ ← formatAux nCtx ctx d₂; pure $ d₁ ++ d₂
   | nCtx, ctx,       group d                  => Format.group <$> formatAux nCtx ctx d

src/Lean/Util/Trace.lean

@@ -91,7 +91,7 @@ private def addNode (oldTraces : PersistentArray TraceElem) (cls : Name) (ref :
     if traces.isEmpty then
       oldTraces
     else
-      let d := MessageData.tagged cls (MessageData.node (traces.toArray.map fun elem => elem.msg))
+      let d := MessageData.tagged cls m!"[{cls}] {MessageData.node (traces.toArray.map fun elem => elem.msg)}"
       oldTraces.push { ref := ref, msg := d }
 
 private def getResetTraces : m (PersistentArray TraceElem) := do
@@ -105,7 +105,7 @@ variable [MonadRef m] [AddMessageContext m] [MonadOptions m]
 def addTrace (cls : Name) (msg : MessageData) : m Unit := do
   let ref ← getRef
   let msg ← addMessageContext msg
-  modifyTraces fun traces => traces.push { ref := ref, msg := MessageData.tagged cls msg }
+  modifyTraces fun traces => traces.push { ref := ref, msg := MessageData.tagged cls m!"[{cls}] {msg}" }
 
 @[inline] def trace (cls : Name) (msg : Unit → MessageData) : m Unit := do
   if (← isTracingEnabledFor cls) then