From b253e31a22024a5bb73b6fa707e6582b4034621b Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 5 Sep 2016 16:24:37 +0200
Subject: feedback: support multiple feedback listeners

So that a module can add his own and look at the traffic
---
 lib/feedback.ml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'lib/feedback.ml')

diff --git a/lib/feedback.ml b/lib/feedback.ml
index 0ec3b2ebe4..4bda936f2b 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -125,8 +125,8 @@ let msg_error   ?loc x = !logger ?loc Error x
 let msg_debug   ?loc x = !logger ?loc Debug x
 
 (** Feeders *)
-let feeder = ref ignore
-let set_feeder f = feeder := f
+let feeders = ref []
+let add_feeder f = feeders := f :: !feeders
 
 let feedback_id    = ref (Edit 0)
 let feedback_route = ref default_route
@@ -135,11 +135,12 @@ let set_id_for_feedback ?(route=default_route) i =
   feedback_id := i; feedback_route := route
 
 let feedback ?id ?route what =
-  !feeder {
+  let m = {
      contents = what;
      route = Option.default !feedback_route route;
      id    = Option.default !feedback_id id;
-  }
+  } in
+  List.iter (fun f -> f m) !feeders
 
 let feedback_logger ?loc lvl msg =
   feedback ~route:!feedback_route ~id:!feedback_id
-- 
cgit v1.2.3