From 4197eb4f94f0bd57b4e9cd391a19968eed373a0d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 6 Nov 2017 14:52:12 +0100 Subject: [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. --- lib/feedback.mli | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'lib/feedback.mli') 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. *) -- cgit v1.2.3