Log4Types.Message

Structured message types for application logging.

Definitions

record SimpleMsg : Type

  A simple log message with severity and text, no structured fields.

Totality: total
Visibility: public export
Constructor: 

MkSimpleMsg : Severity -> String -> SimpleMsg

Projections:

.severity : SimpleMsg -> Severity

.text : SimpleMsg -> String

Hints:

Loggable SimpleMsg

Show SimpleMsg

.severity : SimpleMsg -> Severity

Totality: total
Visibility: public export

severity : SimpleMsg -> Severity

Totality: total
Visibility: public export

.text : SimpleMsg -> String

Totality: total
Visibility: public export

text : SimpleMsg -> String

Totality: total
Visibility: public export

record Msg : Type

  A structured log message with severity, text, and key-value fields.

Totality: total
Visibility: public export
Constructor: 

MkMsg : Severity -> String -> List (String, LogParamValue) -> Msg

Projections:

.fields : Msg -> List (String, LogParamValue)

.severity : Msg -> Severity

.text : Msg -> String

Hints:

Loggable Msg

Show Msg

.severity : Msg -> Severity

Totality: total
Visibility: public export

severity : Msg -> Severity

Totality: total
Visibility: public export

.text : Msg -> String

Totality: total
Visibility: public export

text : Msg -> String

Totality: total
Visibility: public export

.fields : Msg -> List (String, LogParamValue)

Totality: total
Visibility: public export

fields : Msg -> List (String, LogParamValue)

Totality: total
Visibility: public export

fmtMsgWith : (Severity -> String) -> Msg -> String

  Render a Msg as a single line: the severity tag `fmtSev` produces, the
  text, then any fields as `key=value` pairs. `show` uses `fmtSeverity`.

Totality: total
Visibility: public export

mkDebug : String -> Msg

  Create a Debug message with no structured fields.

Totality: total
Visibility: public export

mkInfo : String -> Msg

  Create an Info message with no structured fields.

Totality: total
Visibility: public export

mkWarning : String -> Msg

  Create a Warning message with no structured fields.

Totality: total
Visibility: public export

mkError : String -> Msg

  Create an Error message with no structured fields.

Totality: total
Visibility: public export