diff options
| author | Enrico Tassi | 2014-01-27 17:41:37 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-01-30 17:29:33 +0100 |
| commit | 7516c468528c83593fe4094db35502bc2cda94f8 (patch) | |
| tree | 128aad3ea9f62ebd603fcfc41c7a0a478cb1aaea /lib | |
| parent | 1059ecce2a2662e4d8f335bd4db743df70b100b1 (diff) | |
STM: tell the user if the master is recomputing states validated by workers
When the worker fails, the master may need to recompute some states
the worker has already validates. In this case they are colored
accordingly.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/interface.mli | 1 | ||||
| -rw-r--r-- | lib/serialize.ml | 2 |
2 files changed, 3 insertions, 0 deletions
diff --git a/lib/interface.mli b/lib/interface.mli index 8d250f8507..da09593ba9 100644 --- a/lib/interface.mli +++ b/lib/interface.mli @@ -133,6 +133,7 @@ type feedback_content = | ErrorMsg of Loc.t * string | InProgress of int | SlaveStatus of int * string + | ProcessingInMaster type feedback = { id : edit_or_state_id; diff --git a/lib/serialize.ml b/lib/serialize.ml index 411fb9878e..cfaa40fce1 100644 --- a/lib/serialize.ml +++ b/lib/serialize.ml @@ -328,6 +328,7 @@ let to_loc xml = match xml with let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with | "addedaxiom", _ -> AddedAxiom | "processed", _ -> Processed + | "processinginmaster", _ -> ProcessingInMaster | "incomplete", _ -> Incomplete | "complete", _ -> Complete | "globref", [loc; filepath; modpath; ident; ty] -> @@ -342,6 +343,7 @@ 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" [] | Incomplete -> constructor "feedback_content" "incomplete" [] | Complete -> constructor "feedback_content" "complete" [] | GlobRef(loc, filepath, modpath, ident, ty) -> |