Feedback: API cleaned up, documented and made user extensible

6 files changed, 46 insertions, 41 deletions

diff --git a/lib/feedback.ml b/lib/feedback.ml
index 615886468..4b74078f0 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -58,32 +58,32 @@ type edit_or_state_id = Edit of edit_id | State of state_id
 type route_id = int
 
 type feedback_content =
-  | AddedAxiom
   | Processed
   | Incomplete
   | Complete
-  | GlobRef of Loc.t * string * string * string * string
-  | GlobDef of Loc.t * string * string * string
   | ErrorMsg of Loc.t * string
+  | ProcessingIn of string
   | InProgress of int
-  | SlaveStatus of string * string
-  | ProcessingInMaster
+  | WorkerStatus of string * string
   | Goals of Loc.t * string
-  | StructuredGoals of Loc.t * xml
+  | AddedAxiom
+  | GlobRef of Loc.t * string * string * string * string
+  | GlobDef of Loc.t * string * string * string
   | FileDependency of string option * string
   | FileLoaded of string * string
+  | Custom of Loc.t * string * xml
   | Message of message
 
 type feedback = {
   id : edit_or_state_id;
-  content : feedback_content;
+  contents : feedback_content;
   route : route_id;
 }
 
 let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
   | "addedaxiom", _ -> AddedAxiom
   | "processed", _ -> Processed
-  | "processinginmaster", _ -> ProcessingInMaster
+  | "processingin", [where] -> ProcessingIn (to_string where)
   | "incomplete", _ -> Incomplete
   | "complete", _ -> Complete
   | "globref", [loc; filepath; modpath; ident; ty] ->
@@ -93,11 +93,11 @@ let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
        GlobDef(to_loc loc, to_string ident, to_string secpath, to_string ty)
   | "errormsg", [loc;  s] -> ErrorMsg (to_loc loc, to_string s)
   | "inprogress", [n] -> InProgress (to_int n)
-  | "slavestatus", [ns] ->
+  | "workerstatus", [ns] ->
        let n, s = to_pair to_string to_string ns in
-       SlaveStatus(n,s)
+       WorkerStatus(n,s)
   | "goals", [loc;s] -> Goals (to_loc loc, to_string s)
-  | "structuredgoals", [loc;x]-> StructuredGoals (to_loc loc, x)
+  | "custom", [loc;name;x]-> Custom (to_loc loc, to_string name, x)
   | "filedependency", [from; dep] ->
       FileDependency (to_option to_string from, to_string dep)
   | "fileloaded", [dirpath; filename] ->
@@ -107,7 +107,8 @@ let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
 let of_feedback_content = function
   | AddedAxiom -> constructor "feedback_content" "addedaxiom" []
   | Processed -> constructor "feedback_content" "processed" []
-  | ProcessingInMaster -> constructor "feedback_content" "processinginmaster" []
+  | ProcessingIn where ->
+      constructor "feedback_content" "processingin" [of_string where]
   | Incomplete -> constructor "feedback_content" "incomplete" []
   | Complete -> constructor "feedback_content" "complete" []
   | GlobRef(loc, filepath, modpath, ident, ty) ->
@@ -126,13 +127,13 @@ let of_feedback_content = function
   | ErrorMsg(loc, s) ->
       constructor "feedback_content" "errormsg" [of_loc loc; of_string s]
   | InProgress n -> constructor "feedback_content" "inprogress" [of_int n]
-  | SlaveStatus(n,s) ->
-      constructor "feedback_content" "slavestatus"
+  | WorkerStatus(n,s) ->
+      constructor "feedback_content" "workerstatus"
         [of_pair of_string of_string (n,s)]
   | Goals (loc,s) ->
       constructor "feedback_content" "goals" [of_loc loc;of_string s]
-  | StructuredGoals (loc, x) ->
-      constructor "feedback_content" "structuredgoals" [of_loc loc; x]
+  | Custom (loc, name, x) ->
+      constructor "feedback_content" "custom" [of_loc loc; of_string name; x]
   | FileDependency (from, depends_on) ->
       constructor "feedback_content" "filedependency" [
         of_option of_string from;
@@ -148,7 +149,7 @@ let of_edit_or_state_id = function
   | State id -> ["object","state"], Stateid.to_xml id
 
 let of_feedback msg =
-  let content = of_feedback_content msg.content in
+  let content = of_feedback_content msg.contents in
   let obj, id = of_edit_or_state_id msg.id in
   let route = string_of_int msg.route in
   Element ("feedback", obj @ ["route",route], [id;content])
@@ -156,11 +157,11 @@ let to_feedback xml = match xml with
   | Element ("feedback", ["object","edit";"route",route], [id;content]) -> {
       id = Edit(to_edit_id id);
       route = int_of_string route;
-      content = to_feedback_content content }
+      contents = to_feedback_content 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 }
+      contents = to_feedback_content content }
   | _ -> raise Marshal_error
 
 let is_feedback = function
diff --git a/lib/feedback.mli b/lib/feedback.mli
index bda15fc58..b7822b27b 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -35,25 +35,30 @@ type route_id = int
 val default_route : route_id
 
 type feedback_content =
-  | AddedAxiom
+  (* STM mandatory data (must be displayed) *)
   | Processed
   | Incomplete
   | Complete
-  | GlobRef of Loc.t * string * string * string * string
-  | GlobDef of Loc.t * string * string * string
   | ErrorMsg of Loc.t * string
+  (* STM optional data *)
+  | ProcessingIn of string
   | InProgress of int
-  | SlaveStatus of string * string
-  | ProcessingInMaster
+  | WorkerStatus of string * string
+  (* Generally useful metadata *)
   | Goals of Loc.t * string
-  | StructuredGoals of Loc.t * xml
+  | AddedAxiom
+  | GlobRef of Loc.t * string * string * string * string
+  | GlobDef of Loc.t * string * string * string
   | FileDependency of string option * string
   | FileLoaded of string * string
+  (* Extra metadata *)
+  | Custom of Loc.t * string * xml
+  (* Old generic messages *)
   | Message of message
 
 type feedback = {
   id : edit_or_state_id;       (* The document part concerned *)
-  content : feedback_content;  (* The payload *)
+  contents : feedback_content;  (* The payload *)
   route : route_id;            (* Extra routing info *)
 }
 
diff --git a/lib/flags.ml b/lib/flags.ml
index f95c31d9b..bcd7c59d7 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -85,8 +85,6 @@ let coqtop_ui = ref false
 let ide_slave = ref false
 let ideslave_coqtop_flags = ref None
 
-let feedback_goals = ref false
-
 let time = ref false
 
 let raw_print = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index 757563926..716d04163 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -46,9 +46,6 @@ val coqtop_ui : bool ref
 val ide_slave : bool ref
 val ideslave_coqtop_flags : string option ref
 
-val feedback_goals : bool ref
-
-
 val time : bool ref
 
 val we_are_parsing : bool ref
diff --git a/lib/pp.ml b/lib/pp.ml
index 568d80b62..405eacffe 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -460,17 +460,20 @@ let std_logger lvl msg = std_logger ~id:!feedback_id lvl msg
 (** Feedback *)
 
 let feeder = ref ignore
-let set_id_for_feedback ?(route=0) i = feedback_id := i; feedback_route := route
-let feedback ?state_id ?route what =
+let set_id_for_feedback ?(route=Feedback.default_route) i =
+  feedback_id := i; feedback_route := route
+let feedback ?state_id ?edit_id ?route what =
   !feeder {
-     Feedback.content = what;
+     Feedback.contents = what;
      Feedback.route = Option.default !feedback_route route;
      Feedback.id =
-       match state_id with
-       | Some id -> Feedback.State id
-       | None -> !feedback_id;
+       match state_id, edit_id with
+       | Some id, _ -> Feedback.State id
+       | None, Some eid -> Feedback.Edit eid
+       | None, None -> !feedback_id;
   }
 let set_feeder f = feeder := f
+let get_id_for_feedback () = !feedback_id, !feedback_route
 
 (** Utility *)
 
@@ -480,7 +483,7 @@ let string_of_ppcmds c =
 
 let log_via_feedback () = logger := (fun ~id lvl msg ->
   !feeder {
-     Feedback.content = Feedback.Message {
+     Feedback.contents = Feedback.Message {
        message_level = lvl;
        message_content = string_of_ppcmds msg };
      Feedback.route = !feedback_route;
diff --git a/lib/pp.mli b/lib/pp.mli
index 0293822da..fd529e1d7 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -160,16 +160,17 @@ val is_message : Xml_datatype.xml -> bool
  * Morally the parser gets a string and an edit_id, and gives back an AST.
  * Feedbacks during the parsing phase are attached to this edit_id.
  * The interpreter assignes an exec_id to the ast, and feedbacks happening
- * during interpretation are attached to the exec_id (still unimplemented,
- * since the two phases are performed sequentially) *)
+ * during interpretation are attached to the exec_id.
+ * Only one among state_id and edit_id can be provided. *)
 
 val feedback :
-  ?state_id:Feedback.state_id ->
+  ?state_id:Feedback.state_id -> ?edit_id:Feedback.edit_id ->
   ?route:Feedback.route_id -> Feedback.feedback_content -> unit
 
 val set_id_for_feedback :
   ?route:Feedback.route_id -> Feedback.edit_or_state_id -> unit
 val set_feeder : (Feedback.feedback -> unit) -> unit
+val get_id_for_feedback : unit -> Feedback.edit_or_state_id * Feedback.route_id
 
 (** {6 Utilities} *)