Feedback: API cleaned up, documented and made user extensible

2 files changed, 7 insertions, 79 deletions

diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index fa7aa9584..8b4e0844c 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -135,7 +135,7 @@ module Make(T : Task) = struct
   exception Expired
     
   let report_status ?(id = !Flags.async_proofs_worker_id) s =
-    Pp.feedback ~state_id:Stateid.initial (Feedback.SlaveStatus(id, s))
+    Pp.feedback ~state_id:Stateid.initial (Feedback.WorkerStatus(id, s))
 
   let rec manage_slave ~cancel:cancel_user_req ~die id respawn =
     let ic, oc, proc =
@@ -265,16 +265,8 @@ module Make(T : Task) = struct
   let slave_handshake () = WorkersPool.worker_handshake !slave_ic !slave_oc
 
   let main_loop () =
-    let feedback_queue = ref [] in
     let slave_feeder oc fb =
-      match fb.Feedback.content with
-      | Feedback.Goals _ -> feedback_queue := fb :: !feedback_queue
-      | _ -> Marshal.to_channel oc (RespFeedback fb) []; flush oc in
-    let flush_feeder oc =
-      List.iter (fun fb -> Marshal.to_channel oc (RespFeedback fb) [])
-        !feedback_queue;
-      feedback_queue := [];
-      flush oc in
+      Marshal.to_channel oc (RespFeedback fb) []; flush oc in
     Pp.set_feeder (slave_feeder !slave_oc);
     Pp.log_via_feedback ();
     Universes.set_remote_new_univ_level (bufferize (fun () ->
@@ -290,7 +282,6 @@ module Make(T : Task) = struct
         working := true;
         report_status (name_of_request request);
         let response = slave_respond request in
-        flush_feeder !slave_oc;
         report_status "Idle";
         marshal_response !slave_oc response;
         Ephemeron.clear ()
diff --git a/stm/stm.ml b/stm/stm.ml
index 15637afab..31f90d364 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -58,8 +58,10 @@ let vernac_interp ?proof id ?route { verbose; loc; expr } =
 
 (* Wrapper for Vernac.parse_sentence to set the feedback id *)
 let vernac_parse ?newtip ?route eid s =
-  if Option.is_empty newtip then set_id_for_feedback ?route (Feedback.Edit eid)
-  else set_id_for_feedback ?route (Feedback.State (Option.get newtip));
+  let feedback_id = 
+    if Option.is_empty newtip then Feedback.Edit eid
+    else Feedback.State (Option.get newtip) in
+  set_id_for_feedback ?route feedback_id;
   let pa = Pcoq.Gram.parsable (Stream.of_string s) in
   Flags.with_option Flags.we_are_parsing (fun () ->
     try
@@ -604,6 +606,7 @@ end = struct (* {{{ *)
   let define ?safe_id ?(redefine=false) ?(cache=`No) ?(feedback_processed=true)
         f id
   =
+    feedback ~state_id:id Feedback.(ProcessingIn !Flags.async_proofs_worker_id);
     let str_id = Stateid.to_string id in
     if is_cached id && not redefine then
       anomaly (str"defining state "++str str_id++str" twice");
@@ -636,69 +639,6 @@ end (* }}} *)
 (****************************** CRUFT *****************************************)
 (******************************************************************************)
 
-(* TODO: Currently, this mimics the process_goal function of ide/ide_slave.ml, 
- * but we have the opportunity to provide more structure in the xml, here. *)
-let process_goal sigma g =
-  let env = Goal.V82.env sigma g in
-  let id = Goal.uid g in
-  let ccl =
-    let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in
-    let ccl_string = string_of_ppcmds (Printer.pr_goal_concl_style_env env sigma norm_constr) in
-    Xml_datatype.Element ("conclusion", [], [Xml_datatype.PCData ccl_string]) in
-  let process_hyp env h_env acc =
-    let hyp_string = (string_of_ppcmds (Printer.pr_var_decl env sigma h_env)) in
-    (Xml_datatype.Element ("hypothesis", [], [Xml_datatype.PCData hyp_string])) :: acc in
-  let hyps = Xml_datatype.Element ("hypotheses", [], 
-    (List.rev (Environ.fold_named_context process_hyp env ~init:[]))) in
-  Xml_datatype.Element ("goal", [("id", id)], [hyps; ccl])
-
-let print_goals_of_state, forward_feedback =
-  let already_printed = ref Stateid.Set.empty in
-  let add_to_already_printed =
-    let m = Mutex.create () in
-    fun id ->
-      Mutex.lock m;
-      already_printed := Stateid.Set.add id !already_printed;
-      Mutex.unlock m in
-  (fun id ->
-    if Stateid.Set.mem id !already_printed then ()
-    else begin
-      add_to_already_printed id;
-      try
-        Option.iter (fun { proof = pstate } ->
-          let pfts = Proof_global.proof_of_state pstate in
-          let structured_goals = Proof.map_structured_proof pfts process_goal in
-          let xml_bg_goal = fun (l, r) -> Xml_datatype.Element("bg_goal", [], 
-              [Xml_datatype.Element("left_bg_goals", [], l); 
-               Xml_datatype.Element("right_bg_goals", [], r)]) in
-
-          let xml_structured_goals = Xml_datatype.Element("goals", [],
-            [ Xml_datatype.Element("focussed_goals", [], 
-                structured_goals.Proof.fg_goals);
-              Xml_datatype.Element("bg_goals", [], 
-                List.map xml_bg_goal structured_goals.Proof.bg_goals);
-              Xml_datatype.Element("shelved_goals", [], 
-                structured_goals.Proof.shelved_goals);
-              Xml_datatype.Element("given_up_goals", [], 
-                structured_goals.Proof.given_up_goals)
-            ]
-          ) in
-          Pp.feedback ~state_id:id
-           (Feedback.StructuredGoals (Loc.ghost, xml_structured_goals));
-          Pp.feedback ~state_id:id
-            (Feedback.Goals
-              (Loc.ghost, Pp.string_of_ppcmds
-                (Printer.pr_open_subgoals
-                  ~proof:(Proof_global.proof_of_state pstate) ()))))
-            (VCS.get_info id).state
-      with Proof_global.NoCurrentProof -> ()
-  end),
-  fun id -> function
-    | Feedback.Goals _ as msg ->
-        add_to_already_printed id;
-        Pp.feedback ~state_id:id msg
-    | msg -> Pp.feedback ~state_id:id msg
-
 (* The backtrack module simulates the classic behavior of a linear document *)
 module Backtrack : sig
 
@@ -1657,11 +1597,8 @@ let known_state ?(redefine_qed=false) ~cache id =
     let cache_step =
       if !Flags.async_proofs_cache = Some Flags.Force then `Yes
       else cache_step in
-    if Flags.async_proofs_is_master () then
-      Pp.feedback ~state_id:id Feedback.ProcessingInMaster;
     State.define
       ~cache:cache_step ~redefine:redefine_qed ~feedback_processed step id;
-    if !Flags.feedback_goals then print_goals_of_state id;
     prerr_endline ("reached: "^ Stateid.to_string id) in
   reach ~redefine_qed id