diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-06 14:52:12 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-06 14:55:21 +0100 |
| commit | 4197eb4f94f0bd57b4e9cd391a19968eed373a0d (patch) | |
| tree | 0087e7eb7d8bdc137c922aa923928e98ba724b06 /lib/feedback.mli | |
| parent | e029cf5b417b22ebc65a8193469bbbe450f725ce (diff) | |
[feedback] Helper to print feedback messages in the console.
This is useful for tools such as `coqchk` or `coq_makefile` that want
to handle feedback on their own.
Diffstat (limited to 'lib/feedback.mli')
| -rw-r--r-- | lib/feedback.mli | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/lib/feedback.mli b/lib/feedback.mli index 73b84614f..62b909516 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -99,3 +99,11 @@ val msg_error : ?loc:Loc.t -> Pp.t -> unit val msg_debug : ?loc:Loc.t -> Pp.t -> unit (** For debugging purposes *) + +val console_feedback_listener : Format.formatter -> feedback -> unit +(** Helper for tools willing to print to the feedback system *) + +val warn_no_listeners : bool ref +(** The library will print a warning to the console if no listener is + available by default; ML-clients willing to use Coq without a + feedback handler should set this to false. *) |