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

---
 lib/feedback.ml | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'lib/feedback.ml')

diff --git a/lib/feedback.ml b/lib/feedback.ml
index 4bda936f2..dd1ca2af3 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
 
-- 
cgit v1.2.3