Lean4
@[inherit_doc Mathlib.Linter.linter.style.longLine]
def longLineLinter : Linter where
run :=
withSetOptionIn fun stx ↦ do
unless getLinterValue linter.style.longLine (← getLinterOptions) do
return
if (← MonadState.get).messages.hasErrors then
return
-- The linter ignores the `#guard_msgs` command, in particular its doc-string.
-- The linter still lints the message guarded by `#guard_msgs`.
if stx.isOfKind ``Lean.guardMsgsCmd then
return
-- if the linter reached the end of the file, then we scan the `import` syntax instead
let stx :=
← do
if stx.isOfKind ``Lean.Parser.Command.eoi then
let fileMap ← getFileMap
let (impMods, _) ←
Parser.parseHeader { inputString := fileMap.source, fileName := ← getFileName, fileMap := fileMap }
return impMods.raw
else
return stx
let sstr := stx.getSubstring?
let fm ← getFileMap
let longLines := ((sstr.getD default).splitOn "\n").filter fun line ↦ (100 < (fm.toPosition line.stopPos).column)
for line in longLines do
if (line.splitOn "http").length ≤ 1 then
let stringMsg :=
if line.contains '"' then
"\nYou can use \"string gaps\" to format long strings: within a string quotation, \
using a '\\' at the end of a line allows you to continue the string on the following \
line, removing all intervening whitespace."
else ""
Linter.logLint linter.style.longLine (.ofRange ⟨line.startPos, line.stopPos⟩)
m! "This line exceeds the 100 character limit, please shorten it!{stringMsg}"
