From a5fb20b4ad4a56e15455ca329fbc4d03ac5fe072 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 13 Sep 2016 09:35:05 +0200
Subject: feedback: provide a feeder that prints debug messages

---
 lib/feedback.ml  | 5 +++++
 lib/feedback.mli | 3 +++
 2 files changed, 8 insertions(+)

(limited to 'lib')

diff --git a/lib/feedback.ml b/lib/feedback.ml
index 4bda936f2b..dd1ca2af36 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -128,6 +128,11 @@ let msg_debug   ?loc x = !logger ?loc Debug x
 let feeders = ref []
 let add_feeder f = feeders := f :: !feeders
 
+let debug_feeder = function
+  | { contents = Message (Debug, loc, pp) } ->
+       msg_debug ?loc (Pp.str (Richpp.raw_print pp))
+  | _ -> ()
+
 let feedback_id    = ref (Edit 0)
 let feedback_route = ref default_route
 
diff --git a/lib/feedback.mli b/lib/feedback.mli
index d19517bb94..48b1c19a67 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -86,6 +86,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] *)
-- 
cgit v1.2.3