diff options
Diffstat (limited to 'lib/feedback.ml')
| -rw-r--r-- | lib/feedback.ml | 39 |
1 files changed, 20 insertions, 19 deletions
diff --git a/lib/feedback.ml b/lib/feedback.ml index 6158864681..4b74078f0b 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -58,32 +58,32 @@ type edit_or_state_id = Edit of edit_id | State of state_id type route_id = int type feedback_content = - | AddedAxiom | Processed | Incomplete | Complete - | GlobRef of Loc.t * string * string * string * string - | GlobDef of Loc.t * string * string * string | ErrorMsg of Loc.t * string + | ProcessingIn of string | InProgress of int - | SlaveStatus of string * string - | ProcessingInMaster + | WorkerStatus of string * string | Goals of Loc.t * string - | StructuredGoals of Loc.t * xml + | AddedAxiom + | GlobRef of Loc.t * string * string * string * string + | GlobDef of Loc.t * string * string * string | FileDependency of string option * string | FileLoaded of string * string + | Custom of Loc.t * string * xml | Message of message type feedback = { id : edit_or_state_id; - content : feedback_content; + contents : feedback_content; route : route_id; } let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with | "addedaxiom", _ -> AddedAxiom | "processed", _ -> Processed - | "processinginmaster", _ -> ProcessingInMaster + | "processingin", [where] -> ProcessingIn (to_string where) | "incomplete", _ -> Incomplete | "complete", _ -> Complete | "globref", [loc; filepath; modpath; ident; ty] -> @@ -93,11 +93,11 @@ let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with GlobDef(to_loc loc, to_string ident, to_string secpath, to_string ty) | "errormsg", [loc; s] -> ErrorMsg (to_loc loc, to_string s) | "inprogress", [n] -> InProgress (to_int n) - | "slavestatus", [ns] -> + | "workerstatus", [ns] -> let n, s = to_pair to_string to_string ns in - SlaveStatus(n,s) + WorkerStatus(n,s) | "goals", [loc;s] -> Goals (to_loc loc, to_string s) - | "structuredgoals", [loc;x]-> StructuredGoals (to_loc loc, x) + | "custom", [loc;name;x]-> Custom (to_loc loc, to_string name, x) | "filedependency", [from; dep] -> FileDependency (to_option to_string from, to_string dep) | "fileloaded", [dirpath; filename] -> @@ -107,7 +107,8 @@ let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with let of_feedback_content = function | AddedAxiom -> constructor "feedback_content" "addedaxiom" [] | Processed -> constructor "feedback_content" "processed" [] - | ProcessingInMaster -> constructor "feedback_content" "processinginmaster" [] + | ProcessingIn where -> + constructor "feedback_content" "processingin" [of_string where] | Incomplete -> constructor "feedback_content" "incomplete" [] | Complete -> constructor "feedback_content" "complete" [] | GlobRef(loc, filepath, modpath, ident, ty) -> @@ -126,13 +127,13 @@ 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" + | WorkerStatus(n,s) -> + constructor "feedback_content" "workerstatus" [of_pair of_string of_string (n,s)] | Goals (loc,s) -> constructor "feedback_content" "goals" [of_loc loc;of_string s] - | StructuredGoals (loc, x) -> - constructor "feedback_content" "structuredgoals" [of_loc loc; x] + | Custom (loc, name, x) -> + constructor "feedback_content" "custom" [of_loc loc; of_string name; x] | FileDependency (from, depends_on) -> constructor "feedback_content" "filedependency" [ of_option of_string from; @@ -148,7 +149,7 @@ let of_edit_or_state_id = function | State id -> ["object","state"], Stateid.to_xml id let of_feedback msg = - let content = of_feedback_content msg.content in + let content = of_feedback_content msg.contents in let obj, id = of_edit_or_state_id msg.id in let route = string_of_int msg.route in Element ("feedback", obj @ ["route",route], [id;content]) @@ -156,11 +157,11 @@ let to_feedback xml = match xml with | Element ("feedback", ["object","edit";"route",route], [id;content]) -> { id = Edit(to_edit_id id); route = int_of_string route; - content = to_feedback_content content } + contents = to_feedback_content content } | Element ("feedback", ["object","state";"route",route], [id;content]) -> { id = State(Stateid.of_xml id); route = int_of_string route; - content = to_feedback_content content } + contents = to_feedback_content content } | _ -> raise Marshal_error let is_feedback = function |