feat: message kinds

src/Lean/Log.lean

@@ -66,7 +66,11 @@ def logAt (ref : Syntax) (msgData : MessageData) (severity : MessageSeverity :=
     let endPos := ref.getTailPos?.getD pos
     let fileMap ← getFileMap
     let msgData ← addMessageContext msgData
-    logMessage { fileName := (← getFileName), pos := fileMap.toPosition pos, endPos := fileMap.toPosition endPos, data := msgData, severity := severity }
+    logMessage {
+      fileName := (← getFileName)
+      pos := fileMap.toPosition pos, endPos := fileMap.toPosition endPos
+      kind := msgData.inferKind, data := msgData, severity := severity
+    }
 
 /-- Log a new error message using the given message data. The position is provided by `ref`. -/
 def logErrorAt (ref : Syntax) (msgData : MessageData) : m Unit :=

src/Lean/Message.lean

@@ -116,7 +116,7 @@ variable (p : Name → Bool) in
 /-- Returns true when the message contains a `MessageData.tagged tag ..` constructor where `p tag`
 is true.
 
-This does not descend into lazily generated subtress (`.ofLazy`); message tags
+This does not descend into lazily generated subtrees (`.ofLazy`); message tags
 of interest (like those added by `logLinter`) are expected to be near the root
 of the `MessageData`, and not hidden inside `.ofLazy`.
 -/
@@ -130,6 +130,20 @@ partial def hasTag : MessageData → Bool
   | trace data msg msgs     => p data.cls || hasTag msg || msgs.any hasTag
   | _                       => false
 
+/--
+Returns the top-level tag or trace class of the message.
+If none, returns `Name.anonymous`.
+
+This does not descend into message subtrees (e.g., `.compose`, `.ofLazy`).
+The message kind is expected to describe the whole message.
+-/
+def inferKind : MessageData → Name
+  | withContext _ msg       => inferKind msg
+  | withNamingContext _ msg => inferKind msg
+  | tagged n _              => n
+  | trace data _ _          => data.cls
+  | _                       => .anonymous
+
 /-- An empty message. -/
 def nil : MessageData :=
   ofFormat Format.nil
@@ -307,8 +321,10 @@ structure BaseMessage (α : Type u) where
   endPos        : Option Position := none
   /-- If `true`, report range as given; see `msgToInteractiveDiagnostic`. -/
   keepFullRange : Bool := false
-  severity      : MessageSeverity := MessageSeverity.error
+  severity      : MessageSeverity := .error
   caption       : String          := ""
+  /-- The message kind (e.g., top-level tag or trace class). -/
+  kind          : Name := .anonymous
   /-- The content of the message. -/
   data          : α
   deriving Inhabited, ToJson, FromJson