trailingWhitespaceLinter — Mathlib

Lean4

@[inherit_doc linter.trailingWhitespace]
def trailingWhitespaceLinter : TextbasedLinter := fun opts lines ↦
  Id.run
    (do
      unless getLinterValue linter.trailingWhitespace opts do
        return (#[], none)
      let mut errors := Array.mkEmpty 0
      let mut fixedLines : Vector String lines.size := lines.toVector
      for h : idx in [:lines.size]do
        let line := lines[idx]
        if line.back == ' ' then
          errors := errors.push (StyleError.trailingWhitespace, idx + 1)
          fixedLines := fixedLines.set idx line.trimRight
      return (errors, if errors.size > 0 then some fixedLines.toArray else none))

Похожие утверждения