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

4 files changed, 24 insertions, 9 deletions

diff --git a/lib/feedback.ml b/lib/feedback.ml
index eca9b959f4..6158864681 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 d6d77b7cc4..bda15fc58a 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 8099d75de8..f03fcab3b4 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 ebb6290f92..539ef0f410 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} *)