diff options
| -rw-r--r-- | ide/ide_slave.ml | 2 | ||||
| -rw-r--r-- | lib/feedback.ml | 9 | ||||
| -rw-r--r-- | lib/feedback.mli | 4 | ||||
| -rw-r--r-- | stm/asyncTaskQueue.ml | 4 |
4 files changed, 11 insertions, 8 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 4046ef7ae..bb8723dfe 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 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 diff --git a/lib/feedback.mli b/lib/feedback.mli index d72524e65..d19517bb9 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 2d1f725ef..49b51b171 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 |