Coqide: new feedback mechanism for structured content

This amounts to a new type of message called "feedback" and defined in
Interface to hold structured data.  Coq sends feedback messages
asynchronously (they are all fetched, like regular messages, together
with the main response to a call) and they are related to a specific
sentence by an id.

Other changes:
- CoqOps pushes the sentence to be processed onto the cmd_stack
  before processing it and pulls it back if Coq.intep fails, in this way
  the handler for feedback messages can just look at the cmd_stack
  to find the offset of the sentence to eventually apply the new Gtk.tag.
- The class coqops takes in input a coqtop to set its feedback_handle.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16451 85f007b7-540e-0410-9357-904b9bb8a0f7

14 files changed, 231 insertions, 72 deletions

diff --git a/Makefile.build b/Makefile.build
index b42432d48d..80ff59f716 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -541,7 +541,7 @@ $(COQDOC): $(patsubst %.cma,%$(BESTLIB),$(COQDOCCMO:.cmo=$(BESTOBJ)))
 # fake_ide : for debugging or test-suite purpose, a fake ide simulating
 # a connection to coqtop -ideslave
 
-$(FAKEIDE): lib/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ) lib/xml_utils$(BESTOBJ) lib/serialize$(BESTOBJ) tools/fake_ide$(BESTOBJ)
+$(FAKEIDE): lib/clib$(BESTLIB) lib/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ) tools/fake_ide$(BESTOBJ)
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml,,unix)
 
diff --git a/ide/coq.ml b/ide/coq.ml
index 1219811104..baff54d627 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -275,6 +275,8 @@ type coqtop = {
   sup_args : string list;
   (* called whenever coqtop dies *)
   mutable reset_handler : reset_kind -> unit task;
+  (* called whenever coqtop sends a feedback message *)
+  mutable feedback_handler : Interface.feedback -> unit;
   (* actual coqtop process and its status *)
   mutable handle : handle;
   mutable status : status;
@@ -360,6 +362,11 @@ let handle_intermediate_message logger xml =
   let content = message.Interface.message_content in
   logger level content
 
+let handle_feedback feedback_processor xml =
+  let () = Minilib.log "Handling some feedback" in
+  let feedback = Serialize.to_feedback xml in
+  feedback_processor feedback
+
 let handle_final_answer handle ccb xml =
   let () = Minilib.log "Handling coqtop answer" in
   let () = handle.waiting_for <- None in
@@ -370,7 +377,7 @@ type input_state = {
   mutable lexerror : int option;
 }
 
-let unsafe_handle_input handle state conds =
+let unsafe_handle_input handle feedback_processor state conds =
   let chan = Glib.Io.channel_of_descr handle.cout in
   let () = check_errors conds in
   let s = io_read_all chan in
@@ -392,6 +399,12 @@ let unsafe_handle_input handle state conds =
       let () = state.lexerror <- None in
       let () = handle_intermediate_message logger xml in
       loop ()
+    else if Serialize.is_feedback xml then
+      let remaining = String.sub s l_end (String.length s - l_end) in
+      let () = state.fragment <- remaining in
+      let () = state.lexerror <- None in
+      let () = handle_feedback feedback_processor xml in
+      loop ()
     else
       (* We should have finished decoding s *)
       let () = if not (is_blank s l_end) then raise AnswerWithoutRequest in
@@ -413,7 +426,7 @@ let unsafe_handle_input handle state conds =
     let () = state.lexerror <- Some l_end in
     ()
 
-let install_input_watch handle respawner =
+let install_input_watch handle respawner feedback_processor =
   let io_chan = Glib.Io.channel_of_descr handle.cout in
   let all_conds = [`ERR; `HUP; `IN; `NVAL; `PRI] in (* all except `OUT *)
   let state = {
@@ -429,7 +442,7 @@ let install_input_watch handle respawner =
     if not handle.alive then false (* coqtop already terminated *)
     else
       try
-        let () = unsafe_handle_input handle state conds in
+        let () = unsafe_handle_input handle feedback_processor state conds in
         true
       with e ->
 	let () = Minilib.log ("Coqtop reader failed, resetting: "^print_exception e) in
@@ -472,7 +485,9 @@ let rec respawn_coqtop ?(why=Unexpected) coqtop =
      If not, there isn't much we can do ... *)
   assert (coqtop.handle.alive = true);
   coqtop.status <- New;
-  install_input_watch coqtop.handle (fun () -> respawn_coqtop coqtop);
+  install_input_watch coqtop.handle
+    (fun () -> respawn_coqtop coqtop)
+    (fun msg -> coqtop.feedback_handler msg);
   ignore (coqtop.reset_handler why coqtop.handle (mkready coqtop))
 
 let spawn_coqtop sup_args =
@@ -481,14 +496,18 @@ let spawn_coqtop sup_args =
     handle = spawn_handle sup_args;
     sup_args = sup_args;
     reset_handler = (fun _ _ k -> k ());
+    feedback_handler = (fun _ -> ());
     status = New;
   }
   in
-  install_input_watch ct.handle (fun () -> respawn_coqtop ct);
+  install_input_watch ct.handle
+    (fun () -> respawn_coqtop ct) (fun msg -> ct.feedback_handler msg);
   ct
 
 let set_reset_handler coqtop hook = coqtop.reset_handler <- hook
 
+let set_feedback_handler coqtop hook = coqtop.feedback_handler <- hook
+
 let is_computing coqtop = (coqtop.status = Busy)
 
 (* For closing a coqtop, we don't try to send it a Quit call anymore,
@@ -540,8 +559,8 @@ let eval_call ?(logger=default_logger) call handle k =
   Minilib.log "End eval_call";
   Void
 
-let interp ?(logger=default_logger) ?(raw=false) ?(verbose=true) s h k =
-  eval_call ~logger (Serialize.interp (raw,verbose,s)) h
+let interp ?(logger=default_logger) ?(raw=false) ?(verbose=true) i s h k =
+  eval_call ~logger (Serialize.interp (i,raw,verbose,s)) h
     (function
      | Interface.Good (Util.Inl v) -> k (Interface.Good v)
      | Interface.Good (Util.Inr v) -> k (Interface.Unsafe v)
diff --git a/ide/coq.mli b/ide/coq.mli
index 0210d0b41b..84ef466d72 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -63,6 +63,9 @@ val spawn_coqtop : string list -> coqtop
 val set_reset_handler : coqtop -> (reset_kind -> unit task) -> unit
 (** Register a handler called when a coqtop dies (badly or on purpose) *)
 
+val set_feedback_handler : coqtop -> (Interface.feedback -> unit) -> unit
+(** Register a handler called when coqtop sends a feedback message *)
+
 val init_coqtop : coqtop -> unit task -> unit
 (** Finish initializing a freshly spawned coqtop, by running a first task on it.
     The task should run its inner continuation at the end. *)
@@ -113,8 +116,11 @@ val try_grab : coqtop -> unit task -> (unit -> unit) -> unit
 type 'a query = 'a Interface.value task
 (** A type abbreviation for coqtop specific answers *)
 
-val interp : ?logger:Ideutils.logger -> ?raw:bool -> ?verbose:bool ->
-  string -> string query
+val interp :
+  ?logger:Ideutils.logger ->
+  ?raw:bool ->
+  ?verbose:bool ->
+    int -> string -> string query
 val rewind : int -> int query
 val status : Interface.status query
 val goals : Interface.goals option query
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 3e76b94b20..2647f923c0 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -11,11 +11,40 @@ open Ideutils
 
 type flag = [ `COMMENT | `UNSAFE ]
 
-type ide_info = {
-  start : GText.mark;
-  stop : GText.mark;
-  flags : flag list;
-}
+module SentenceId : sig
+
+  type sentence = private {
+    start : GText.mark;
+    stop : GText.mark;
+    mutable flags : flag list;
+    id : int;
+  }
+
+  val mk_sentence :
+    start:GText.mark -> stop:GText.mark -> flag list -> sentence
+  val set_flags : sentence -> flag list -> unit
+
+end = struct
+
+  type sentence = {
+    start : GText.mark;
+    stop : GText.mark;
+    mutable flags : flag list;
+    id : int;
+  }
+
+  let id = ref 0
+  let mk_sentence ~start ~stop flags = decr id; {
+    start = start;
+    stop = stop;
+    flags = flags;
+    id = !id;
+  }
+
+  let set_flags s f = s.flags <- f
+
+end
+open SentenceId
 
 let prefs = Preferences.current
 
@@ -39,6 +68,7 @@ class coqops
   (_script:Wg_ScriptView.script_view)
   (_pv:Wg_ProofView.proof_view)
   (_mv:Wg_MessageView.message_view)
+  (_ct:Coq.coqtop)
   get_filename =
 object(self)
   val script = _script
@@ -48,6 +78,9 @@ object(self)
 
   val cmd_stack = Stack.create ()
 
+  initializer
+    Coq.set_feedback_handler _ct self#process_feedback
+
   method private get_start_of_input =
     buffer#get_iter_at_mark (`NAME "start_of_input")
 
@@ -81,7 +114,8 @@ object(self)
         flash_info "This error is so nasty that I can't even display it."
       else messages#add s;
     in
-    let query = Coq.interp ~logger:messages#push ~raw:true ~verbose:false phrase in
+    let query =
+      Coq.interp ~logger:messages#push ~raw:true ~verbose:false 0 phrase in
     let next = function
     | Interface.Fail (_, err) -> display_error err; Coq.return ()
     | Interface.Good msg | Interface.Unsafe msg ->
@@ -103,12 +137,12 @@ object(self)
         let is_comment =
           stop#backward_char#has_tag Tags.Script.comment_sentence
         in
-        let payload = {
-          start = `MARK (buffer#create_mark start);
-          stop = `MARK (buffer#create_mark stop);
-          flags = if is_comment then [`COMMENT] else [];
-        } in
-        Queue.push payload queue;
+        let sentence =
+          mk_sentence
+            ~start:(`MARK (buffer#create_mark start))
+            ~stop:(`MARK (buffer#create_mark stop))
+            (if is_comment then [`COMMENT] else []) in
+        Queue.push sentence queue;
         if not stop#is_end then loop (succ len) stop
     in
     try loop 0 self#get_start_of_input with Exit -> ()
@@ -123,22 +157,37 @@ object(self)
       buffer#delete_mark sentence.stop;
     done
 
-  method private commit_queue_transaction queue sentence newflags =
+  method private mark_as_needed sentence =
+    let start = buffer#get_iter_at_mark sentence.start in
+    let stop = buffer#get_iter_at_mark sentence.stop in
+    let tag =
+      if List.mem `UNSAFE sentence.flags then Tags.Script.unjustified
+      else Tags.Script.processed in
+    buffer#apply_tag tag ~start ~stop
+
+  method private process_feedback msg =
+    let id = msg.Interface.edit_id in
+    if id = 0 || Stack.is_empty cmd_stack then () else
+    let sentence =
+      let last_sentence = Stack.top cmd_stack in
+      if last_sentence.id = id then Some last_sentence else None in
+    match msg.Interface.content, sentence with
+    | Interface.AddedAxiom, Some sentence ->
+        set_flags sentence (CList.add_set `UNSAFE sentence.flags);
+        self#mark_as_needed sentence
+    | Interface.Processed, Some sentence -> self#mark_as_needed sentence
+    | _, None -> Minilib.log "Coqide/Coq is really asynchronous now!"
+         (* In this case we shoud look for (exec_)id into cmd_stack *)
+
+  method private commit_queue_transaction sentence =
     (* A queued command has been successfully done, we push it to [cmd_stack].
        We reget the iters here because Gtk is unable to warranty that they
        were not modified meanwhile. Not really necessary but who knows... *)
+    self#mark_as_needed sentence;
     let start = buffer#get_iter_at_mark sentence.start in
     let stop = buffer#get_iter_at_mark sentence.stop in
-    let sentence = { sentence with flags = newflags @ sentence.flags } in
-    let tag =
-      if List.mem `UNSAFE newflags then Tags.Script.unjustified
-      else Tags.Script.processed
-    in
     buffer#move_mark ~where:stop (`NAME "start_of_input");
-    buffer#apply_tag tag ~start ~stop;
-    buffer#remove_tag Tags.Script.to_process ~start ~stop;
-    ignore (Queue.pop queue);
-    Stack.push sentence cmd_stack
+    buffer#remove_tag Tags.Script.to_process ~start ~stop
 
   method private process_error queue phrase loc msg =
     Coq.bind (Coq.return ()) (function () ->
@@ -153,6 +202,10 @@ object(self)
         buffer#apply_tag Tags.Script.error ~start ~stop;
         buffer#place_cursor ~where:start
     in
+    let sentence = Stack.pop cmd_stack in
+    let start = buffer#get_iter_at_mark sentence.start in
+    let stop = buffer#get_iter_at_mark sentence.stop in
+    buffer#remove_tag Tags.Script.to_process ~start ~stop;
     self#discard_command_queue queue;
     pop_info ();
     position_error loc;
@@ -183,9 +236,10 @@ object(self)
         let () = script#recenter_insert in
         self#show_goals
       else
-        let sentence = Queue.peek queue in
+        let sentence = Queue.pop queue in
+        Stack.push sentence cmd_stack;
         if List.mem `COMMENT sentence.flags then
-          (self#commit_queue_transaction queue sentence []; loop ())
+          (self#commit_queue_transaction sentence; loop ())
         else
           (* If the line is not a comment, we interpret it. *)
           let phrase =
@@ -193,17 +247,18 @@ object(self)
             let stop = buffer#get_iter_at_mark sentence.stop in
             start#get_slice ~stop
           in
-          let commit_and_continue msg flags =
+          let commit_and_continue msg =
             push_msg Interface.Notice msg;
-            self#commit_queue_transaction queue sentence flags;
+            self#commit_queue_transaction sentence;
             loop ()
           in
-          let query = Coq.interp ~logger:push_msg ~verbose phrase in
+          let query = Coq.interp ~logger:push_msg ~verbose sentence.id phrase in
           let next = function
-          | Interface.Good msg -> commit_and_continue msg []
-          | Interface.Unsafe msg -> commit_and_continue msg [`UNSAFE]
-          | Interface.Fail (loc, msg) ->
-            self#process_error queue phrase loc msg
+          | Interface.Good msg -> commit_and_continue msg
+          | Interface.Unsafe msg ->
+              set_flags sentence (CList.add_set `UNSAFE sentence.flags);
+              commit_and_continue msg
+          | Interface.Fail (loc, msg) -> self#process_error queue phrase loc msg
           in
           Coq.bind query next
     in
@@ -329,12 +384,12 @@ object(self)
       buffer#apply_tag tag ~start ~stop;
       if self#get_insert#compare stop <= 0 then
         buffer#place_cursor ~where:stop;
-      let ide_payload = {
-        start = `MARK (buffer#create_mark start);
-        stop = `MARK (buffer#create_mark stop);
-        flags = [];
-      } in
-      Stack.push ide_payload cmd_stack;
+      let sentence =
+        mk_sentence
+          ~start:(`MARK (buffer#create_mark start))
+          ~stop:(`MARK (buffer#create_mark stop))
+          [] in
+      Stack.push sentence cmd_stack;
       messages#clear;
       self#show_goals
     in
@@ -345,7 +400,7 @@ object(self)
     in
     let try_phrase phrase stop more =
       let action = log "Sending to coq now" in
-      let query = Coq.interp ~verbose:false phrase in
+      let query = Coq.interp ~verbose:false 0 phrase in
       let next = function
       | Interface.Fail (l, str) ->
         display_error (l, str);
@@ -400,7 +455,7 @@ object(self)
       | Interface.Good true | Interface.Unsafe true -> Coq.return ()
       | Interface.Good false | Interface.Unsafe false ->
         let cmd = Printf.sprintf "Add LoadPath \"%s\". "  dir in
-        let cmd = Coq.interp cmd in
+        let cmd = Coq.interp 0 cmd in
         let next = function
         | Interface.Fail (l, str) ->
           messages#set ("Couln't add loadpath:\n"^str);
diff --git a/ide/coqOps.mli b/ide/coqOps.mli
index 7e47ca23f7..48a07f48ba 100644
--- a/ide/coqOps.mli
+++ b/ide/coqOps.mli
@@ -25,5 +25,6 @@ class coqops :
   Wg_ScriptView.script_view ->
   Wg_ProofView.proof_view ->
   Wg_MessageView.message_view ->
+  coqtop ->
   (unit -> string option) ->
   ops
diff --git a/ide/session.ml b/ide/session.ml
index 8eeb3c6f9e..4e95fefca3 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -155,8 +155,8 @@ let create file coqtop_args =
   let finder = new Wg_Find.finder (script :> GText.view) in
   let fops = new FileOps.fileops (buffer :> GText.buffer) file reset in
   let _ = fops#update_stats in
-  let cops = new CoqOps.coqops script proof messages (fun () -> fops#filename)
-  in
+  let cops =
+    new CoqOps.coqops script proof messages coqtop (fun () -> fops#filename) in
   let _ = Coq.set_reset_handler coqtop cops#handle_reset_initial in
   let _ = Coq.init_coqtop coqtop cops#initialize in
   {
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index e0a7427798..dd8896cba0 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -111,10 +111,9 @@ object(self)
 	if String.get com (String.length com - 1) = '.'
 	then com ^ " " else com ^ " " ^ entry#text ^" . "
       in
-      let log level message = result#buffer#insert (message^"\n")
-      in
+      let log level message = result#buffer#insert (message^"\n") in
       let process =
-	Coq.bind (Coq.interp ~logger:log ~raw:true phrase) (function
+	Coq.bind (Coq.interp ~logger:log ~raw:true 0 phrase) (function
           | Interface.Fail (l,str) ->
             result#buffer#insert ("Error while interpreting "^phrase^":\n"^str);
 	    Coq.return ()
diff --git a/lib/interface.mli b/lib/interface.mli
index 349f7baf98..d54fb84760 100644
--- a/lib/interface.mli
+++ b/lib/interface.mli
@@ -103,7 +103,7 @@ type coq_info = {
   compile_date : string;
 }
 
-(** Coq messages *)
+(** Coq unstructured messages *)
 
 type message_level =
   | Debug of string
@@ -117,6 +117,20 @@ type message = {
   message_content : string;
 }
 
+(** Coq "semantic" infos obtained during parsing/execution *)
+type edit_id = int
+
+type feedback_content =
+  | AddedAxiom
+  | Processed
+
+type feedback = {
+  edit_id : edit_id;
+  content : feedback_content;
+}
+
+(** Calls result *)
+
 type location = (int * int) option (* start and end of the error *)
 
 type 'a value =
@@ -126,18 +140,16 @@ type 'a value =
 
 (* Request/Reply message protocol between Coq and CoqIde *)
 
-(** Running a command (given as a string).
-    The 1st flag indicates whether to use "raw" mode
-    (less sanity checks, no impact on the undo stack).
-    Suitable e.g. for queries, or for the Set/Unset
+(** Running a command (given as its id and its text).
+    "raw" mode (less sanity checks, no impact on the undo stack)
+    is suitable for queries, or for the Set/Unset
     of display options that coqide performs all the time.
-    The 2nd flag controls the verbosity.
     The returned string contains the messages produced
-    by this command, but not the updated goals (they are
+    but not the updated goals (they are
     to be fetch by a separated [current_goals]). *)
-type interp_sty = raw * verbose * string
 (* spiwack: [Inl] for safe and [Inr] for unsafe. *)
 type interp_rty = (string,string) Util.union
+type interp_sty = edit_id * raw * verbose * string
 
 (** Backtracking by at least a certain number of phrases.
     No finished proofs will be re-opened. Instead,
diff --git a/lib/pp.ml b/lib/pp.ml
index 85c623f0c8..c346943e15 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -354,6 +354,18 @@ let msg_debug x = !logger (Debug "_") x
 
 let set_logger l = logger := l
 
+(** Feedback *)
+
+let feeder = ref ignore
+let feedback_id = ref 0
+let set_id_for_feedback i = feedback_id := i
+let feedback what =
+  !feeder {
+     Interface.edit_id = !feedback_id;
+     Interface.content = what
+  }
+let set_feeder f = feeder := f
+
 (** Utility *)
 
 let string_of_ppcmds c =
diff --git a/lib/pp.mli b/lib/pp.mli
index b46115fd4a..bc7441836b 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -106,6 +106,22 @@ val std_logger : logger
 
 val set_logger : logger -> unit
 
+(** {6 Feedback sent, even asynchronously, to the user interface *)
+
+(* This stuff should be available to most of the system, line msg_* above.
+ * But I'm unsure this is the right place, especially for the global edit_id.
+ *
+ * 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) *)
+
+val feedback : Interface.feedback_content -> unit
+
+val set_id_for_feedback : Interface.edit_id -> unit
+val set_feeder : (Interface.feedback -> unit) -> unit
+
 (** {6 Utilities} *)
 
 val string_of_ppcmds : std_ppcmds -> string
diff --git a/lib/serialize.ml b/lib/serialize.ml
index 0b9cc0a14f..fd8c7e7e4e 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -359,9 +359,10 @@ let to_value f = function
 | _ -> raise Marshal_error
 
 let of_call = function
-| Interp (raw, vrb, cmd) ->
+| Interp (id,raw, vrb, cmd) ->
   let flags = (bool_arg "raw" raw) @ (bool_arg "verbose" vrb) in
-  Element ("call", ("val", "interp") :: flags, [PCData cmd])
+  Element ("call", ("val", "interp") :: ("id", string_of_int id) :: flags,
+  [PCData cmd])
 | Rewind n ->
   Element ("call", ("val", "rewind") :: ["steps", string_of_int n], [])
 | Goal () ->
@@ -394,9 +395,10 @@ let to_call = function
   let ans = massoc "val" attrs in
   begin match ans with
   | "interp" ->
+    let id = List.assoc "id" attrs in
     let raw = List.mem_assoc "raw" attrs in
     let vrb = List.mem_assoc "verbose" attrs in
-    Interp (raw, vrb, raw_string l)
+    Interp (int_of_string id, raw, vrb, raw_string l)
   | "rewind" ->
     let steps = int_of_string (massoc "steps" attrs) in
     Rewind steps
@@ -525,6 +527,30 @@ let is_message = function
 | Element ("message", _, _) -> true
 | _ -> false
 
+let to_feedback_content xml = do_match xml "feedback_content"
+  (fun s args -> match s with
+  | "addedaxiom" -> AddedAxiom
+  | "processed" -> Processed
+  | _ -> raise Marshal_error)
+
+let of_feedback_content = function
+| AddedAxiom -> constructor "feedback_content" "addedaxiom" []
+| Processed -> constructor "feedback_content" "processed" []
+
+let of_feedback msg =
+  let content = of_feedback_content msg.content in
+  Element ("feedback", ["id",string_of_int msg.edit_id], [content])
+
+let to_feedback xml = match xml with
+| Element ("feedback", ["id",id], [content]) ->
+  { edit_id = int_of_string id;
+    content = to_feedback_content content }
+| _ -> raise Marshal_error
+
+let is_feedback = function
+| Element ("feedback", _, _) -> true
+| _ -> false
+
 (** Conversions between ['a value] and xml answers
 
   When decoding an xml answer, we dynamically check that it is compatible
@@ -617,10 +643,10 @@ let pr_pair pr1 pr2 (a,b) = "("^pr1 a^","^pr2 b^")"
 let pr_union pr1 pr2 = function Util.Inl x -> pr1 x | Util.Inr x -> pr2 x
 
 let pr_call = function
-  | Interp (r,b,s) ->
+  | Interp (id,r,b,s) ->
     let raw = if r then "RAW" else "" in
     let verb = if b then "" else "SILENT" in
-    "INTERP"^raw^verb^" ["^s^"]"
+    "INTERP"^raw^verb^" "^string_of_int id^" ["^s^"]"
   | Rewind i -> "REWIND "^(string_of_int i)
   | Goal _ -> "GOALS"
   | Evars _ -> "EVARS"
diff --git a/lib/serialize.mli b/lib/serialize.mli
index 3ecf066bef..4af4d09749 100644
--- a/lib/serialize.mli
+++ b/lib/serialize.mli
@@ -48,6 +48,10 @@ val of_message : message -> xml
 val to_message : xml -> message
 val is_message : xml -> bool
 
+val of_feedback : feedback -> xml
+val to_feedback : xml -> feedback
+val is_feedback : xml -> bool
+
 val of_answer : 'a call -> 'a value -> xml
 val to_answer : xml -> 'a call -> 'a value
 
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index d3b927a590..6a4823ee0f 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -31,6 +31,8 @@ let eval_call call coqtop =
       let content = message.Interface.message_content in
       let () = logger level content in
       loop ()
+    else if Serialize.is_feedback xml then
+      loop ()
     else (Serialize.to_answer xml call)
   in
   let res = loop () in
@@ -38,10 +40,10 @@ let eval_call call coqtop =
   match res with Interface.Fail _ -> exit 1 | _ -> ()
 
 let commands =
-  [ "INTERPRAWSILENT", (fun s -> eval_call (Serialize.interp (true,false,s)));
-    "INTERPRAW", (fun s -> eval_call (Serialize.interp (true,true,s)));
-    "INTERPSILENT", (fun s -> eval_call (Serialize.interp (false,false,s)));
-    "INTERP", (fun s -> eval_call (Serialize.interp (false,true,s)));
+  [ "INTERPRAWSILENT", (fun s -> eval_call (Serialize.interp (0,true,false,s)));
+    "INTERPRAW", (fun s -> eval_call (Serialize.interp (0,true,true,s)));
+    "INTERPSILENT", (fun s -> eval_call (Serialize.interp (0,false,false,s)));
+    "INTERP", (fun s -> eval_call (Serialize.interp (0,false,true,s)));
     "REWIND", (fun s -> eval_call (Serialize.rewind (int_of_string s)));
     "GOALS", (fun _ -> eval_call (Serialize.goals ()));
     "HINTS", (fun _ -> eval_call (Serialize.hints ()));
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index bd3067d969..fd5fa85cba 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -114,7 +114,8 @@ let coqide_cmd_checks (loc,ast) =
 
 (** Interpretation (cf. [Ide_intf.interp]) *)
 
-let interp (raw,verbosely,s) =
+let interp (id,raw,verbosely,s) =
+  Pp.set_id_for_feedback id;
   let pa = Pcoq.Gram.parsable (Stream.of_string s) in
   let loc_ast = Vernac.parse_sentence (pa,None) in
   if not raw then coqide_cmd_checks loc_ast;
@@ -338,6 +339,11 @@ let slave_logger level message =
   Xml_utils.print_xml !orig_stdout xml;
   flush !orig_stdout
 
+let slave_feeder msg =
+  let xml = Serialize.of_feedback msg in
+  Xml_utils.print_xml !orig_stdout xml;
+  flush !orig_stdout
+
 (** The main loop *)
 
 (** Exceptions during eval_call should be converted into [Interface.Fail]
@@ -348,6 +354,7 @@ let loop () =
   init_signal_handler ();
   catch_break := false;
   Pp.set_logger slave_logger;
+  Pp.set_feeder slave_feeder;
   (* We'll handle goal fetching and display in our own way *)
   Vernacentries.enable_goal_printing := false;
   Vernacentries.qed_display_script := false;