Lean4
/-- Try parsing an `ErrorContext` from a string: return `some` if successful, `none` otherwise. -/
def parse?_errorContext (line : String) : Option ErrorContext :=
Id.run
(do
let parts := line.split (· == ' ')
match parts with
| filename :: ":" :: "line" :: lineNumber :: ":" :: errorCode :: ":" :: _errorMessage =>
-- Turn the filename into a path. In general, this is ambiguous if we don't know if we're
-- dealing with e.g. Windows or POSIX paths. In our setting, this is fine, since no path
-- component contains any path separator.
let path :=
mkFilePath
(filename.split (FilePath.pathSeparators.contains ·))
-- Parse the error kind from the error code, ugh.
-- NB: keep this in sync with `StyleError.errorCode` above!
let err : Option StyleError :=
match errorCode with
-- Use default values for parameters which are ignored for comparing style exceptions.
-- NB: keep this in sync with `compare` above!
| "ERR_ADN" => some (StyleError.adaptationNote)
| "ERR_SEM" => some (StyleError.semicolon)
| "ERR_TWS" => some (StyleError.trailingWhitespace)
| "ERR_WIN" => some (StyleError.windowsLineEnding)
| _ => none
match String.toNat? lineNumber with
| some n =>
err.map fun e ↦ (ErrorContext.mk e n path)
| _ =>
none
| _ =>
none)
