Feedback
val default_route : route_id
type feedback_content =
| Processed |
| Incomplete |
| Complete |
| ProcessingIn of string |
| InProgress of int |
| WorkerStatus of string * string |
| AddedAxiom |
| GlobRef of Loc.t * string * string * string * string |
| GlobDef of Loc.t * string * string * string |
| FileDependency of string option * string |
| FileLoaded of string * string |
| Custom of Loc.t option * string * Xml_datatype.xml |
| Message of level * Loc.t option * Quickfix.t list * Pp.t |
val add_feeder : (feedback -> unit) -> int
add_feeder f
adds a feeder listiner f
, returning its id
val feedback : ?did:doc_id -> ?id:Stateid.t -> ?route:route_id -> feedback_content -> unit
feedback ?did ?sid ?route fb
produces feedback fb
, with route
and did, sid
set appropiatedly, if absent, it will use the defaults set by set_id_for_feedback
set_id_for_feedback route id
Set the defaults for feedback
Message that displays information, usually in verbose mode, such as Foobar
is defined
Message that should be displayed, such as Print Foo
or Show Bar
.
val msg_warning : ?loc:Loc.t -> ?quickfix:Quickfix.t list -> Pp.t -> unit
Message indicating that something went wrong, but without serious consequences. A list of quick fixes, in the VSCode sense, can be provided
val console_feedback_listener : Stdlib.Format.formatter -> feedback -> unit
Helper for tools willing to print to the feedback system