Lean4
@[inherit_doc linter.whitespaceBeforeSemicolon]
def semicolonLinter : TextbasedLinter := fun opts lines ↦
Id.run
(do
unless getLinterValue linter.whitespaceBeforeSemicolon opts do
return (#[], none)
let mut errors := Array.mkEmpty 0
let mut fixedLines := lines
for h : idx in [:lines.size]do
let line := lines[idx]
let pos :=
line.find
(· == ';')
-- Future: also lint for a semicolon *not* followed by a space or ⟩.
if pos != line.endPos && line.get (line.prev pos) == ' ' then
errors :=
errors.push
(StyleError.semicolon, idx + 1)
-- We spell the bad string pattern this way to avoid the linter firing on itself.
fixedLines := fixedLines.set! idx (line.replace (⟨[' ', ';']⟩ : String) ";")
return (errors, if errors.size > 0 then some fixedLines else none))
