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 | |
| 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.
| -rw-r--r-- | ide/coqOps.ml | 4 | ||||
| -rw-r--r-- | lib/interface.mli | 1 | ||||
| -rw-r--r-- | lib/serialize.ml | 2 | ||||
| -rw-r--r-- | toplevel/stm.ml | 2 |
4 files changed, 9 insertions, 0 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml index be9075279b..347459a65f 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -348,6 +348,10 @@ object(self) remove_flag sentence `PROCESSING; remove_flag sentence `ERROR; self#mark_as_needed sentence + | ProcessingInMaster, Some (id,sentence) -> + log "ProcessingInMaster" id; + add_flag sentence `PROCESSING; + self#mark_as_needed sentence | Incomplete, Some (id, sentence) -> log "Incomplete" id; add_flag sentence `INCOMPLETE; 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) -> diff --git a/toplevel/stm.ml b/toplevel/stm.ml index ac041a9f78..3f0c232773 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -1308,6 +1308,8 @@ let known_state ?(redefine_qed=false) ~cache id = inject_non_pstate s ), cache in + if !Flags.async_proofs_mode = Flags.APonParallel 0 then + Pp.feedback ~state_id:id Interface.ProcessingInMaster; State.define ~cache:cache_step ~redefine:redefine_qed step id; prerr_endline ("reached: "^ Stateid.to_string id) in reach ~redefine_qed id |