Lean4
/-- Output the formatted error message, containing its context.
`style` specifies if the error should be formatted for humans to read, github problem matchers
to consume, or for the style exceptions file. -/
def outputMessage (errctx : ErrorContext) (style : ErrorFormat) : String :=
let errorMessage := errctx.error.errorMessage
match style with
| ErrorFormat.github =>
-- We are outputting for github: duplicate file path, line number and error code,
-- so that they are also visible in the plain text output.
let path := errctx.path
let nr := errctx.lineNumber
let code := errctx.error.errorCode
s! "::ERR file={path },line={nr },code={code }::{path }:{nr } {code }: {errorMessage}"
| ErrorFormat.exceptionsFile =>
-- Produce an entry in the exceptions file: with error code and "line" in front of the number.
s! "{errctx.path } : line {errctx.lineNumber } : {errctx.error.errorCode } : {errorMessage}"
| ErrorFormat.humanReadable =>
-- Print for humans: clickable file name and omit the error code
s! "error: {errctx.path }:{errctx.lineNumber }: {errorMessage}"
