Feedback message: hold extra info to help routing

PIDE based GUIs can take advantage of multiple panels and get
some feedback routed there. E.g. query panel

3 files changed, 25 insertions, 19 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index ad3ecfd457..4b4d50c41d 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -36,7 +36,7 @@ type ast = { verbose : bool; loc : Loc.t; mutable expr : vernac_expr }
 let pr_ast { expr } = pr_vernac expr
 
 (* Wrapper for Vernacentries.interp to set the feedback id *)
-let vernac_interp ?proof id { verbose; loc; expr } =
+let vernac_interp ?proof id ?route { verbose; loc; expr } =
   let rec internal_command = function
     | VernacResetName _ | VernacResetInitial | VernacBack _
     | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _
@@ -46,7 +46,7 @@ let vernac_interp ?proof id { verbose; loc; expr } =
   if internal_command expr then begin
     prerr_endline ("ignoring " ^ string_of_ppcmds(pr_vernac expr))
   end else begin
-    Pp.set_id_for_feedback (Feedback.State id);
+    Pp.set_id_for_feedback ?route (Feedback.State id);
     Aux_file.record_in_aux_set_at loc;
     prerr_endline ("interpreting " ^ string_of_ppcmds(pr_vernac expr));
     let interp = Hook.get f_interp in
@@ -57,9 +57,9 @@ let vernac_interp ?proof id { verbose; loc; expr } =
   end
 
 (* Wrapper for Vernac.parse_sentence to set the feedback id *)
-let vernac_parse ?newtip eid s =
-  if Option.is_empty newtip then set_id_for_feedback (Feedback.Edit eid)
-  else set_id_for_feedback (Feedback.State (Option.get newtip));
+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 pa = Pcoq.Gram.parsable (Stream.of_string s) in
   Flags.with_option Flags.we_are_parsing (fun () ->
     try
@@ -1834,19 +1834,19 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
           anomaly(str"classifier: VtBack + VtLater must imply part_of_script")
 
       (* Query *)
-      | VtQuery (false,report_id), VtNow when tty = true ->
+      | VtQuery (false,(report_id,route)), VtNow when tty = true ->
           finish ();
-          (try Future.purify (vernac_interp report_id)
+          (try Future.purify (vernac_interp report_id ~route)
                   { verbose = true; loc; expr }
            with e when Errors.noncritical e ->
              let e = Errors.push e in
              raise(State.exn_on report_id e)); `Ok
-      | VtQuery (false,report_id), VtNow ->
-          (try vernac_interp report_id x
+      | VtQuery (false,(report_id,route)), VtNow ->
+          (try vernac_interp report_id ~route x
            with e when Errors.noncritical e ->
              let e = Errors.push e in
              raise(State.exn_on report_id e)); `Ok
-      | VtQuery (true,report_id), w ->
+      | VtQuery (true,(report_id,_)), w ->
           assert(Stateid.equal report_id Stateid.dummy);
           let id = VCS.new_node ~id:newtip () in
           let queue =
@@ -1976,11 +1976,12 @@ let print_ast id =
 
 let stop_worker n = Slaves.cancel_worker n
 
-let query ~at ?(report_with=Stateid.dummy) s =
+let query ~at ?(report_with=(Stateid.dummy,Feedback.default_route)) s =
   Future.purify (fun s ->
     if Stateid.equal at Stateid.dummy then finish ()
     else Reach.known_state ~cache:`Yes at;
-    let _, ast as loc_ast = vernac_parse ~newtip:report_with 0 s in
+    let newtip, route = report_with in
+    let _, ast as loc_ast = vernac_parse ~newtip ~route 0 s in
     let clas = classify_vernac ast in
     match clas with
     | VtStm (w,_), _ ->
diff --git a/stm/stm.mli b/stm/stm.mli
index 57e70d24eb..2e133f1eb7 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -25,7 +25,8 @@ val add : ontop:Stateid.t -> ?newtip:Stateid.t -> ?check:(located_vernac_expr ->
 (* parses and executes a command at a given state, throws away its side effects
    but for the printings.  Feedback is sent with report_with (defaults to dummy
    state id)  *)
-val query : at:Stateid.t -> ?report_with:Stateid.t -> string -> unit
+val query :
+  at:Stateid.t -> ?report_with:(Stateid.t * Feedback.route_id) -> string -> unit
 
 (* [edit_at id] is issued to change the editing zone.  [`NewTip] is returned if
    the requested id is the new document tip hence the document portion following
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index e810e59072..733f3e4412 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -22,11 +22,13 @@ let string_of_vernac_type = function
   | VtProofStep false -> "ProofStep"
   | VtProofStep true -> "ProofStep (parallel)"
   | VtProofMode s -> "ProofMode " ^ s
-  | VtQuery (b,_) -> "Query" ^ string_of_in_script b
+  | VtQuery (b,(id,route)) ->
+      "Query " ^ string_of_in_script b ^ " report " ^ Stateid.to_string id ^
+      " route " ^ string_of_int route
   | VtStm ((VtFinish|VtJoinDocument|VtObserve _|VtPrintDag|VtWait), b) ->
-      "Stm" ^ string_of_in_script b
-  | VtStm (VtPG, b) -> "Stm PG" ^ string_of_in_script b
-  | VtStm (VtBack _, b) -> "Stm Back" ^ string_of_in_script b
+      "Stm " ^ string_of_in_script b
+  | VtStm (VtPG, b) -> "Stm PG " ^ string_of_in_script b
+  | VtStm (VtBack _, b) -> "Stm Back " ^ string_of_in_script b
 
 let string_of_vernac_when = function
   | VtLater -> "Later"
@@ -92,7 +94,8 @@ let rec classify_vernac e =
     | VernacEndProof _ | VernacExactProof _ -> VtQed VtKeep, VtLater
     (* Query *)
     | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _
-    | VernacCheckMayEval _ -> VtQuery (true,Stateid.dummy), VtLater
+    | VernacCheckMayEval _ ->
+        VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater
     (* ProofStep *)
     | VernacSolve (SelectAllParallel,_,_) -> VtProofStep true, VtLater
     | VernacProof _ 
@@ -215,5 +218,6 @@ let rec classify_vernac e =
       make_polymorphic res
     else res
 
-let classify_as_query = VtQuery (true,Stateid.dummy), VtLater
+let classify_as_query =
+  VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater
 let classify_as_sideeff = VtSideff [], VtLater