feat: the trailingWhitespace linter

Author: adomani

Batteries/Linter.lean

@@ -1,2 +1,3 @@
+import Batteries.Linter.TrailingWhitespace
 import Batteries.Linter.UnreachableTactic
 import Batteries.Linter.UnnecessarySeqFocus

Batteries/Linter/TrailingWhitespace.lean

@@ -0,0 +1,50 @@
+import Lean.Elab.Command
+import Lean.Linter.Util
+
+/-!
+#  The "trailingWhitespace" linter
+
+The "trailingWhitespace" linter emits a warning whenever a line ends with a space or a file
+does not end with a line break.
+-/
+
+open Lean Elab
+
+namespace Mathlib.Linter
+
+/--
+The "trailingWhitespace" linter emits a warning whenever a line ends with a space or a file
+does not end with a line break.
+-/
+register_option linter.trailingWhitespace : Bool := {
+  defValue := true
+  descr := "enable the trailingWhitespace linter"
+}
+
+namespace TrailingWhitespace
+
+@[inherit_doc Mathlib.Linter.linter.trailingWhitespace]
+def trailingWhitespaceLinter : Linter where run := withSetOptionIn fun stx ↦ do
+  unless Linter.getLinterValue linter.trailingWhitespace (← getOptions) do
+    return
+  if (← get).messages.hasErrors then
+    return
+  let srg := stx.getRange?.getD default
+  let fm ← getFileMap
+  for lb in fm.positions do
+    if srg.contains lb then
+    let last : Substring := { str := fm.source, startPos := ⟨lb.1 - 2⟩, stopPos := ⟨lb.1 - 1⟩ }
+    if last.toString == " " then
+      Linter.logLint linter.trailingWhitespace (.ofRange ⟨⟨lb.1 - 2⟩, ⟨lb.1 - 1⟩⟩)
+        m!"Lines should not end with a space."
+  unless Parser.isTerminalCommand stx do return
+  let (backBack, back) := (fm.positions.pop.back, fm.positions.back)
+  let rg : String.Range := ⟨back - ⟨1⟩, back⟩
+  if backBack != back then
+    Linter.logLint linter.trailingWhitespace (.ofRange rg) m!"Files should end with a line-break."
+
+initialize addLinter trailingWhitespaceLinter
+
+end TrailingWhitespace
+
+end Mathlib.Linter