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

1 files changed, 6 insertions, 4 deletions

diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index d3b927a59..6a4823ee0 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 ()));