diff options
Diffstat (limited to 'stm')
-rw-r--r-- | stm/stm.ml | 4 | ||||
-rw-r--r-- | stm/stm.mli | 3 |
2 files changed, 5 insertions, 2 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 3386044f2..7e17fa2f5 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2373,6 +2373,7 @@ let finish () = | _ -> () let wait () = + finish (); Slaves.wait_all_done (); VCS.print () @@ -2386,7 +2387,6 @@ let rec join_admitted_proofs id = | _ -> join_admitted_proofs view.next let join () = - finish (); wait (); stm_prerr_endline (fun () -> "Joining the environment"); Global.join_safe_environment (); @@ -2486,7 +2486,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) match c with (* Joining various parts of the document *) | VtStm (VtJoinDocument, b), VtNow -> join (); `Ok - | VtStm (VtWait, b), VtNow -> finish (); wait (); `Ok + | VtStm (VtWait, b), VtNow -> wait (); `Ok | VtStm ((VtJoinDocument|VtWait),_), VtLater -> anomaly(str"classifier: join actions cannot be classified as VtLater.") diff --git a/stm/stm.mli b/stm/stm.mli index 188b176ba..3f01fca01 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -51,6 +51,9 @@ val edit_at : Stateid.t -> [ `NewTip | `Focus of focus ] (* Evaluates the tip of the current branch *) val finish : unit -> unit +(* Internal use (fake_ide) only, do not use *) +val wait : unit -> unit + val observe : Stateid.t -> unit val stop_worker : string -> unit |