New feedback message: SlaveStatus

To tell the gui what a slave is doing

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

2 files changed, 7 insertions, 0 deletions

diff --git a/lib/interface.mli b/lib/interface.mli
index 69eaac789..a8e3d72bd 100644
--- a/lib/interface.mli
+++ b/lib/interface.mli
@@ -126,6 +126,7 @@ type feedback_content =
   | GlobRef of Loc.t * string * string * string * string
   | ErrorMsg of Loc.t * string
   | InProgress of int
+  | SlaveStatus of int * string
 
 type feedback = {
   id : edit_or_state_id;
diff --git a/lib/serialize.ml b/lib/serialize.ml
index aded47984..88bf87c13 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -329,6 +329,9 @@ let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
          to_string modpath, to_string ident, to_string ty)
   | "errormsg", [loc;  s] -> ErrorMsg (to_loc loc, to_string s)
   | "inprogress", [n] -> InProgress (to_int n)
+  | "slavestatus", [ns] ->
+       let n, s = to_pair to_int to_string ns in
+       SlaveStatus(n,s)
   | _ -> raise Marshal_error)
 let of_feedback_content = function
   | AddedAxiom -> constructor "feedback_content" "addedaxiom" []
@@ -343,6 +346,9 @@ 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"
+        [of_pair of_int of_string (n,s)]
 
 let of_feedback msg =
   let content = of_feedback_content msg.content in