fix(linter): "(invalid MessageData.lazy, missing context)" (#838)

leanprover-community · Jun 12, 2024 · 42b5ddd · 42b5ddd
1 parent f96a344
commit 42b5ddd
Showing 1 changed file with 4 additions and 2 deletions.
diff --git a/Batteries/Tactic/Lint/Frontend.lean b/Batteries/Tactic/Lint/Frontend.lean
@@ -125,9 +125,11 @@ def printWarning (declName : Name) (warning : MessageData) (useErrorFormat : Boo
   (filePath : System.FilePath := default) : CoreM MessageData := do
   if useErrorFormat then
     if let some range ← findDeclarationRanges? declName then
-      return m!"{filePath}:{range.range.pos.line}:{range.range.pos.column + 1}: error: {
+      let msg ← addMessageContextPartial
+        m!"{filePath}:{range.range.pos.line}:{range.range.pos.column + 1}: error: {
           ← mkConstWithLevelParams declName} {warning}"
-  pure m!"#check {← mkConstWithLevelParams declName} /- {warning} -/"
+      return msg
+  addMessageContextPartial m!"#check {← mkConstWithLevelParams declName} /- {warning} -/"
 
 /-- Formats a map of linter warnings using `print_warning`, sorted by line number. -/
 def printWarnings (results : HashMap Name MessageData) (filePath : System.FilePath := default)