From 72f471f42d7825b9ef370fb5a64acbd155d9140e Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 27 Nov 2014 11:00:46 +0100
Subject: AsyncTaskQueue: parsin can also happen in the workers now

---
 stm/asyncTaskQueue.ml  | 9 ++-------
 stm/asyncTaskQueue.mli | 3 +--
 stm/stm.ml             | 6 +++++-
 stm/stm.mli            | 3 +--
 4 files changed, 9 insertions(+), 12 deletions(-)

diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index d870ff92b0..298fa8237f 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -37,8 +37,7 @@ module type Task = sig
   val on_marshal_error : string -> task -> unit
   val on_slave_death : task option -> [ `Exit of int | `Stay ]
   val on_task_cancellation_or_expiration : task option -> unit
-  val forward_feedback :
-    Stateid.t -> Feedback.route_id -> Feedback.feedback_content -> unit
+  val forward_feedback : Feedback.feedback -> unit
  
   (* run by the worker *)
   val perform : request -> response
@@ -193,11 +192,7 @@ module Make(T : Task) = struct
                   (CList.init 10 (fun _ ->
                      Universes.new_univ_level (Global.current_dirpath ()))));
                 loop ()
-            | RespFeedback ({ Feedback.id = Feedback.State state_id;
-                              Feedback.route = rid } as fbk) ->
-                T.forward_feedback state_id rid fbk.Feedback.content;
-                loop ()
-            | RespFeedback _ -> Errors.anomaly (str"Parsing in master process")
+            | RespFeedback fbk -> T.forward_feedback fbk; loop ()
           in
             loop ()
         with
diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli
index 172e1035ec..ee364ff19c 100644
--- a/stm/asyncTaskQueue.mli
+++ b/stm/asyncTaskQueue.mli
@@ -29,8 +29,7 @@ module type Task = sig
   val on_marshal_error : string -> task -> unit
   val on_slave_death : task option -> [ `Exit of int | `Stay ]
   val on_task_cancellation_or_expiration : task option -> unit
-  val forward_feedback :
-    Stateid.t -> Feedback.route_id -> Feedback.feedback_content -> unit
+  val forward_feedback : Feedback.feedback -> unit
  
   (* run by the worker *)
   val perform : request -> response
diff --git a/stm/stm.ml b/stm/stm.ml
index 09005386e8..2d1d8aefea 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -29,7 +29,11 @@ let state_computed, state_computed_hook = Hook.make
     feedback ~state_id Feedback.Processed) ()
 
 let forward_feedback, forward_feedback_hook = Hook.make
- ~default:(fun state_id route msg -> feedback ~state_id ~route msg) ()
+ ~default:(function
+    | { Feedback.id = Feedback.Edit edit_id; route; contents } ->
+          feedback ~edit_id ~route contents
+    | { Feedback.id = Feedback.State state_id; route; contents } ->
+          feedback ~state_id ~route contents) ()
 
 let parse_error, parse_error_hook = Hook.make
  ~default:(function
diff --git a/stm/stm.mli b/stm/stm.mli
index 5696f35c1e..3dd0764dd4 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -102,8 +102,7 @@ val parse_error_hook :
 val execution_error_hook : (Stateid.t -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t
 
 (* Messages from the workers to the master *)
-val forward_feedback_hook :
-  (Stateid.t -> Feedback.route_id -> Feedback.feedback_content -> unit) Hook.t
+val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t
 
 type state = {
   system : States.state;
-- 
cgit v1.2.3