diff options
Diffstat (limited to 'lib/feedback.mli')
| -rw-r--r-- | lib/feedback.mli | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/lib/feedback.mli b/lib/feedback.mli index d19517bb94..b4bed8793d 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -36,7 +36,6 @@ type feedback_content = | InProgress of int | WorkerStatus of string * string (* Generally useful metadata *) - | Goals of Loc.t * string | AddedAxiom | GlobRef of Loc.t * string * string * string * string | GlobDef of Loc.t * string * string * string @@ -72,11 +71,8 @@ val set_logger : logger -> unit (** [std_logger] standard logger to [stdout/stderr] *) val std_logger : logger -val color_terminal_logger : logger -(* This logger will apply the proper {!Pp_style} tags, and in - particular use the formatters {!Pp_control.std_ft} and - {!Pp_control.err_ft} to display those messages. Be careful this is - not compatible with the Emacs mode! *) +(** [init_color_output ()] Enable color in the std_logger *) +val init_color_output : unit -> unit (** [feedback_logger] will produce feedback messages instead IO events *) val feedback_logger : logger @@ -86,6 +82,9 @@ val emacs_logger : logger (** [add_feeder] feeders observe the feedback *) val add_feeder : (feedback -> unit) -> unit +(** Prints feedback messages of kind Message(Debug,_) using msg_debug *) +val debug_feeder : feedback -> unit + (** [feedback ?id ?route fb] produces feedback fb, with [route] and [id] set appropiatedly, if absent, it will use the defaults set by [set_id_for_feedback] *) |