gillian » Gillian » Debugger » Logging

Module Debugger.Logging

module JsonMap : sig ... end

A mapping of strings to Yojson values

val log :
  ?v:bool ->
  ((?json:JsonMap.t -> ('a, Stdlib.Format.formatter, unit) Stdlib.format -> 'a) ->
    unit) ->
  unit

Sends a log message to the debugger frontend via a custom event. Optionally includes some accompanying JSON.

A couple of things to bear in mind:

• If debugging isn't enabled (or setup hasn't been called yet), this function does nothing, i.e. the passed function isn't called.
• The message is sent asynchronously; it may, for example, arrive after an error is raised, despite being called before.
• The message is also logged to the debugger log file (see to_file), though without the JSON - if JSON is provided, the message is suffixed with (+).

val to_file : string -> unit

Logs a message to the debugger log file (gillian-debugger.log in the current working directory). This is more reliable than log, but more unwieldy, and doesn't support attached JSON.

val show_report : ?v:bool -> Logging.Report_id.t -> string -> unit

Logs a message (as with log), but attaches the type and (parsed) content of the specified report.

val failwith : (unit -> JsonMap.t) -> string -> 'a

Raises an exception with a string message and attached JSON.

Note that if debugging isn't enabled, then the JSON function is ignored, and a regular `Failure` is raised instead.