From b43676541010546b9d41281c1689c242511fa39e Mon Sep 17 00:00:00 2001 From: gareuselesinge Date: Tue, 22 Oct 2013 09:22:09 +0000 Subject: 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 --- lib/interface.mli | 1 + lib/serialize.ml | 6 ++++++ 2 files changed, 7 insertions(+) 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 -- cgit v1.2.3