fix: logging of linter warnings

src/Lean/Linter/Builtin.lean

@@ -25,10 +25,8 @@ def suspiciousUnexpanderPatterns : Linter := fun cmdStx => do
       | `(`($patHead:ident))         => pure patHead
       | _                            => continue
 
-    if let some range := patHead.raw.getRange? then
-      publishMessage
-        "Unexpanders should match the function name against an antiquotation `$_` so as to be independent of the specific pretty printing of the name. [linter.suspiciousUnexpanderPatterns]"
-        range
+    logLint linter.suspiciousUnexpanderPatterns patHead
+      "Unexpanders should match the function name against an antiquotation `$_` so as to be independent of the specific pretty printing of the name."
 
 builtin_initialize addLinter suspiciousUnexpanderPatterns
 

src/Lean/Linter/MissingDocs.lean

@@ -99,7 +99,7 @@ builtin_initialize
   mkAttr false `missingDocsHandler
 
 def lint (stx : Syntax) (msg : String) : CommandElabM Unit :=
-  logWarningAt stx s!"missing doc string for {msg} [linter.missingDocs]"
+  logLint linter.missingDocs stx m!"missing doc string for {msg}"
 
 def lintNamed (stx : Syntax) (msg : String) : CommandElabM Unit :=
   lint stx s!"{msg} {stx.getId}"

src/Lean/Linter/UnusedVariables.lean

@@ -235,8 +235,7 @@ def unusedVariables : Linter := fun cmdStx => do
       continue
 
     -- publish warning if variable is unused and not ignored
-    publishMessage (.tagged decl_name%
-      m!"unused variable `{localDecl.userName}` [linter.unusedVariables]") range
+    logLint linter.unusedVariables declStx m!"unused variable `{localDecl.userName}`"
 
   return ()
 where
@@ -256,4 +255,4 @@ builtin_initialize addLinter unusedVariables
 end Linter
 
 def MessageData.isUnusedVariableWarning (msg : MessageData) : Bool :=
-  msg.hasTag (· == ``Linter.unusedVariables)
+  msg.hasTag (· == Linter.linter.unusedVariables.name)

src/Lean/Linter/Util.lean

@@ -15,12 +15,8 @@ def getLinterValue (opt : Lean.Option Bool) (o : Options) : Bool := o.get opt.na
 
 open Lean.Elab Lean.Elab.Command
 
-def publishMessage
-  (content : MessageData) (range : String.Range) (severity : MessageSeverity := .warning) : CommandElabM Unit :=
-do
-  let ctx := (← read)
-  let messages := (← get).messages |>.add (mkMessageCore ctx.fileName ctx.fileMap content severity range.start range.stop)
-  modify ({ · with messages := messages })
+def logLint (linterOption : Lean.Option Bool) (stx : Syntax) (msg : MessageData) : CommandElabM Unit :=
+  logWarningAt stx (.tagged linterOption.name m!"{msg} [{linterOption.name}]")
 
 /-- Go upwards through the given `tree` starting from the smallest node that
 contains the given `range` and collect all `MacroExpansionInfo`s on the way up.

tests/lean/warningAsError.lean

@@ -8,3 +8,6 @@ def g (x : Nat) := x + 1
 set_option warningAsError true
 
 #eval g 0 -- error
+
+set_option linter.unusedVariables true
+def h (unused : Nat) := 0  -- error

tests/lean/warningAsError.lean.expected.out

@@ -2,3 +2,4 @@ warningAsError.lean:6:6-6:7: warning: `g` has been deprecated, use `f` instead
 1
 warningAsError.lean:10:6-10:7: error: `g` has been deprecated, use `f` instead
 1
+warningAsError.lean:13:7-13:13: error: unused variable `unused` [linter.unusedVariables]