pre-stage0 error name PR review edits

Author: jrr6

src/Lean/Log.lean

@@ -94,7 +94,7 @@ private def MessageData.appendDescriptionWidgetIfNamed (msg : MessageData) : Mes
     }
     -- Note: we do not generate corresponding message data for the widget because it pollutes
     -- console output
-    msg.appendPreservingKind <| .ofWidget inst .nil
+    msg.composePreservingKind <| .ofWidget inst .nil
   | none => msg
 
 /--
@@ -137,6 +137,15 @@ protected def «logNamedErrorAt» (ref : Syntax) (name : Name) (msgData : Messag
 def logWarningAt [MonadOptions m] (ref : Syntax) (msgData : MessageData) : m Unit := do
   logAt ref msgData .warning
 
+/--
+Log a named error warning using the given message data. The position is provided by `ref`.
+
+Note: Use the macro `logNamedWarningAt`, which validates error names, instead of calling this function
+directly.
+-/
+protected def «logNamedWarningAt» (ref : Syntax) (name : Name) (msgData : MessageData) : m Unit :=
+  logAt ref (msgData.tagWithErrorName name) MessageSeverity.warning
+
 /-- Log a new information message using the given message data. The position is provided by `ref`. -/
 def logInfoAt (ref : Syntax) (msgData : MessageData) : m Unit :=
   logAt ref msgData MessageSeverity.information
@@ -164,6 +173,15 @@ protected def «logNamedError» (name : Name) (msgData : MessageData) : m Unit :
 def logWarning [MonadOptions m] (msgData : MessageData) : m Unit := do
   log msgData .warning
 
+/--
+Log a named warning using the given message data. The position is provided by `getRef`.
+
+Note: Use the macro `logNamedWarning`, which validates error names, instead of calling this function
+directly.
+-/
+protected def «logNamedWarning» (name : Name) (msgData : MessageData) : m Unit :=
+  log (msgData.tagWithErrorName name) MessageSeverity.warning
+
 /-- Log a new information message using the given message data. The position is provided by `getRef`. -/
 def logInfo (msgData : MessageData) : m Unit :=
   log msgData MessageSeverity.information

src/Lean/Message.lean

@@ -170,12 +170,12 @@ def isTrace : MessageData → Bool
   | _                       => false
 
 /--
-`appendPreservingKind msg msg'` appends the contents of `msg'` to the end of `msg` but ensures that
+`composePreservingKind msg msg'` appends the contents of `msg'` to the end of `msg` but ensures that
 the resulting message preserves the kind (as given by `MessageData.kind`) of `msg`.
 -/
-def appendPreservingKind : MessageData → MessageData → MessageData
-  | withContext ctx msg     , msg' => withContext ctx (appendPreservingKind msg msg')
-  | withNamingContext nc msg, msg' => withNamingContext nc (appendPreservingKind msg msg')
+def composePreservingKind : MessageData → MessageData → MessageData
+  | withContext ctx msg     , msg' => withContext ctx (composePreservingKind msg msg')
+  | withNamingContext nc msg, msg' => withNamingContext nc (composePreservingKind msg msg')
   | tagged t msg            , msg' => tagged t (compose msg msg')
   | msg                     , msg' => compose msg msg'
 

src/Lean/Parser/Term.lean

@@ -1119,12 +1119,29 @@ associated error explanation exists. The message may be passed as an interpolate
 /--
 Logs an error, tagging the message as a named error with the specified name and validating that an
 associated error explanation exists. The error name must be followed by a `Syntax` at which the
-error is to be thrown. The message is the final argument and may be passed as an interpolated string
+error is to be logged. The message is the final argument and may be passed as an interpolated string
 or a `MessageData` term.
 -/
 @[builtin_term_parser] def logNamedErrorAtMacro := leading_parser
   "logNamedErrorAt " >> termParser maxPrec >> ppSpace >> identWithPartialTrailingDot >> ppSpace >> (interpolatedStr termParser <|> termParser maxPrec)
 
+/--
+Logs a warning, tagging the message as a named diagnostic with the specified name and validating
+that an associated error explanation exists. The message may be passed as an interpolated string or
+a `MessageData` term. The result of `getRef` is used as position information.
+-/
+@[builtin_term_parser] def logNamedWarningMacro := leading_parser
+  "logNamedWarning " >> identWithPartialTrailingDot >> ppSpace >> (interpolatedStr termParser <|> termParser maxPrec)
+
+/--
+Logs a warning, tagging the message as a named diagnostic with the specified name and validating
+that an associated error explanation exists. The error name must be followed by a `Syntax` at which
+the warning is to be logged. The message is the final argument and may be passed as an interpolated
+string or a `MessageData` term.
+-/
+@[builtin_term_parser] def logNamedWarningAtMacro := leading_parser
+  "logNamedWarningAt " >> termParser maxPrec >> ppSpace >> identWithPartialTrailingDot >> ppSpace >> (interpolatedStr termParser <|> termParser maxPrec)
+
 end Term
 
 @[builtin_term_parser default+1] def Tactic.quot : Parser := leading_parser