aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/feedback.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2016-09-05 16:24:37 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2016-09-05 16:37:00 +0200
commitb253e31a22024a5bb73b6fa707e6582b4034621b (patch)
tree6064122d2531d77ab981321c69df8ec7cc6db947 /lib/feedback.ml
parent6f393734e54146c4d26325aea006368380d97280 (diff)
feedback: support multiple feedback listeners
So that a module can add his own and look at the traffic
Diffstat (limited to 'lib/feedback.ml')
-rw-r--r--lib/feedback.ml9
1 files changed, 5 insertions, 4 deletions
diff --git a/lib/feedback.ml b/lib/feedback.ml
index 0ec3b2ebe..4bda936f2 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