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

5 files changed, 83 insertions, 13 deletions

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