feedback: support multiple feedback listeners

So that a module can add his own and look at the traffic

4 files changed, 11 insertions, 8 deletions

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 4046ef7aec..bb8723dfe6 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -499,7 +499,7 @@ let loop () =
   let xml_ic = Xml_parser.make (Xml_parser.SLexbuf in_lb) in
   let () = Xml_parser.check_eof xml_ic false in
   Feedback.set_logger (slave_logger xml_oc);
-  Feedback.set_feeder (slave_feeder xml_oc);
+  Feedback.add_feeder (slave_feeder xml_oc);
   (* We'll handle goal fetching and display in our own way *)
   Vernacentries.enable_goal_printing := false;
   Vernacentries.qed_display_script := false;
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
diff --git a/lib/feedback.mli b/lib/feedback.mli
index d72524e65f..d19517bb94 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -83,8 +83,8 @@ val feedback_logger : logger
 val emacs_logger    : logger
 
 
-(** [set_feeder] A feeder processes the feedback, [ignore] by default *)
-val set_feeder : (feedback -> unit) -> unit
+(** [add_feeder] feeders observe the feedback *)
+val add_feeder : (feedback -> unit) -> unit
 
 (** [feedback ?id ?route fb] produces feedback fb, with [route] and
     [id] set appropiatedly, if absent, it will use the defaults set by
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 2d1f725ef0..49b51b1715 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -299,10 +299,12 @@ module Make(T : Task) = struct
     Pool.worker_handshake (Option.get !slave_ic) (Option.get !slave_oc)
 
   let main_loop () =
+    (* We pass feedback to master *)
     let slave_feeder oc fb =
       Marshal.to_channel oc (RespFeedback fb) []; flush oc in
-    Feedback.set_feeder (fun x -> slave_feeder (Option.get !slave_oc) x);
+    Feedback.add_feeder (fun x -> slave_feeder (Option.get !slave_oc) x);
     Feedback.set_logger Feedback.feedback_logger;
+    (* We ask master to allocate universe identifiers *)
     Universes.set_remote_new_univ_level (bufferize (fun () ->
       marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel;
       match unmarshal_more_data (Option.get !slave_ic) with