diff --git a/src/Lean/Elab/Log.lean b/src/Lean/Elab/Log.lean index 8eac22779c..a328ede568 100644 --- a/src/Lean/Elab/Log.lean +++ b/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 diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index 96ffd51627..1f975cd899 100644 --- a/src/Lean/Message.lean +++ b/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 diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean index 053c1ec84e..d70fabcdf6 100644 --- a/src/Lean/Util/Trace.lean +++ b/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