Lean4
/-- Return if `line` looks like a correct authors line in a copyright header.
The `offset` input is used to shift the position information of the `Syntax` that the command
produces.
`authorsLineChecks` computes a position for its warning *relative to `line`*.
The `offset` input passes on the starting position of `line` in the whole file.
-/
def authorsLineChecks (line : String) (offset : String.Pos) : Array (Syntax × String) :=
Id.run
(do
-- We cannot reasonably validate the author names, so we look only for a few common mistakes:
-- the line starting wrongly, double spaces, using ' and ' between names,
-- and ending the line with a period.
let mut stxs := #[]
if !line.startsWith "Authors: " then
stxs :=
stxs.push
(toSyntax line (line.take "Authors: ".length) offset, s!"The authors line should begin with 'Authors: '")
if (line.splitOn " ").length != 1 then
stxs := stxs.push (toSyntax line " " offset, s!"Double spaces are not allowed.")
if (line.splitOn " and ").length != 1 then
stxs := stxs.push (toSyntax line " and " offset, s!"Please, do not use 'and'; use ',' instead.")
if line.back == '.' then
stxs := stxs.push (toSyntax line "." offset, s!"Please, do not end the authors' line with a period.")
return stxs)
