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

9 files changed, 52 insertions, 31 deletions

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 028668746..5cd34038f 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -458,7 +458,7 @@ type vernac_type =
   | VtQuery of vernac_part_of_script * report_with
   | VtStm of vernac_control * vernac_part_of_script
   | VtUnknown
-and report_with = Stateid.t (* report feedback on a different id *)
+and report_with = Stateid.t * Feedback.route_id (* feedback on id/route *)
 and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *)
 and vernac_start = string * opacity_guarantee * Id.t list
 and vernac_sideff_type = Id.t list
diff --git a/lib/feedback.ml b/lib/feedback.ml
index eca9b959f..615886468 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -55,6 +55,7 @@ let is_message = function
 type edit_id = int
 type state_id = Stateid.t
 type edit_or_state_id = Edit of edit_id | State of state_id
+type route_id = int
 
 type feedback_content =
   | AddedAxiom
@@ -76,6 +77,7 @@ type feedback_content =
 type feedback = {
   id : edit_or_state_id;
   content : feedback_content;
+  route : route_id;
 }
 
 let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
@@ -148,13 +150,16 @@ let of_edit_or_state_id = function
 let of_feedback msg =
   let content = of_feedback_content msg.content in
   let obj, id = of_edit_or_state_id msg.id in
-  Element ("feedback", obj, [id;content])
+  let route = string_of_int msg.route in
+  Element ("feedback", obj @ ["route",route], [id;content])
 let to_feedback xml = match xml with
-  | Element ("feedback", ["object","edit"], [id;content]) -> {
+  | Element ("feedback", ["object","edit";"route",route], [id;content]) -> {
       id = Edit(to_edit_id id);
+      route = int_of_string route;
       content = to_feedback_content content }
-  | Element ("feedback", ["object","state"], [id;content]) -> { 
+  | Element ("feedback", ["object","state";"route",route], [id;content]) -> { 
       id = State(Stateid.of_xml id);
+      route = int_of_string route;
       content = to_feedback_content content }
   | _ -> raise Marshal_error
 
@@ -162,3 +167,4 @@ let is_feedback = function
   | Element ("feedback", _, _) -> true
   | _ -> false
 
+let default_route = 0
diff --git a/lib/feedback.mli b/lib/feedback.mli
index d6d77b7cc..bda15fc58 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -30,6 +30,9 @@ val is_message : xml -> bool
 type edit_id = int
 type state_id = Stateid.t
 type edit_or_state_id = Edit of edit_id | State of state_id
+type route_id = int
+
+val default_route : route_id
 
 type feedback_content =
   | AddedAxiom
@@ -49,8 +52,9 @@ type feedback_content =
   | Message of message
 
 type feedback = {
-  id : edit_or_state_id;
-  content : feedback_content;
+  id : edit_or_state_id;       (* The document part concerned *)
+  content : feedback_content;  (* The payload *)
+  route : route_id;            (* Extra routing info *)
 }
 
 val of_feedback : feedback -> xml
diff --git a/lib/pp.ml b/lib/pp.ml
index 8099d75de..f03fcab3b 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -386,6 +386,7 @@ let std_logger ~id:_ level msg = match level with
 let logger = ref std_logger
 
 let feedback_id = ref (Feedback.Edit 0)
+let feedback_route = ref Feedback.default_route
 
 let msg_info x = !logger ~id:!feedback_id Info x
 let msg_notice x = !logger ~id:!feedback_id Notice x
@@ -400,10 +401,11 @@ let std_logger lvl msg = std_logger ~id:!feedback_id lvl msg
 (** Feedback *)
 
 let feeder = ref ignore
-let set_id_for_feedback i = feedback_id := i
-let feedback ?state_id what =
+let set_id_for_feedback ?(route=0) i = feedback_id := i; feedback_route := route
+let feedback ?state_id ?route what =
   !feeder {
      Feedback.content = what;
+     Feedback.route = Option.default !feedback_route route;
      Feedback.id =
        match state_id with
        | Some id -> Feedback.State id
@@ -422,6 +424,7 @@ let log_via_feedback () = logger := (fun ~id lvl msg ->
      Feedback.content = Feedback.Message {
        message_level = lvl;
        message_content = string_of_ppcmds msg };
+     Feedback.route = !feedback_route;
      Feedback.id = id })
 
 (* Copy paste from Util *)
diff --git a/lib/pp.mli b/lib/pp.mli
index ebb6290f9..539ef0f41 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -134,9 +134,11 @@ val is_message : Xml_datatype.xml -> bool
  * since the two phases are performed sequentially) *)
 
 val feedback :
-  ?state_id:Feedback.state_id -> Feedback.feedback_content -> unit
+  ?state_id:Feedback.state_id ->
+  ?route:Feedback.route_id -> Feedback.feedback_content -> unit
 
-val set_id_for_feedback : Feedback.edit_or_state_id -> unit
+val set_id_for_feedback :
+  ?route:Feedback.route_id -> Feedback.edit_or_state_id -> unit
 val set_feeder : (Feedback.feedback -> unit) -> unit
 
 (** {6 Utilities} *)
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 96ab4f1e1..0bb4fc35c 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -779,7 +779,7 @@ VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF
   | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods(l) ] ->
     [ let (k,set,cst,pre,post,power,sign, div) = process_ring_mods l in
       add_theory id (ic t) set k cst (pre,post) power sign div]
-  | [ "Print" "Rings" ] => [Vernacexpr.VtQuery (true, Stateid.dummy), Vernacexpr.VtLater] -> [
+  | [ "Print" "Rings" ] => [Vernac_classifier.classify_as_query] -> [
     msg_notice (strbrk "The following ring structures have been declared:");
     Spmap.iter (fun fn fi ->
       msg_notice (hov 2
@@ -1110,7 +1110,7 @@ VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF
 | [ "Add" "Field" ident(id) ":" constr(t) field_mods(l) ] ->
   [ let (k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods l in
     add_field_theory id (ic t) set k cst_tac inj (pre,post) power sign div]
-| [ "Print" "Fields" ] => [Vernacexpr.VtQuery (true, Stateid.dummy), Vernacexpr.VtLater] -> [
+| [ "Print" "Fields" ] => [Vernac_classifier.classify_as_query] -> [
     msg_notice (strbrk "The following field structures have been declared:");
     Spmap.iter (fun fn fi ->
       msg_notice (hov 2
diff --git a/stm/stm.ml b/stm/stm.ml
index ad3ecfd45..4b4d50c41 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 57e70d24e..2e133f1eb 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 e810e5907..733f3e441 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