diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/future.ml | 4 | ||||
| -rw-r--r-- | lib/pp.mli | 3 | ||||
| -rw-r--r-- | lib/remoteCounter.ml | 4 |
3 files changed, 5 insertions, 6 deletions
diff --git a/lib/future.ml b/lib/future.ml index 23d089fb6b..247b139798 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -112,8 +112,8 @@ let create_delegate ?(blocking=true) ~name fix_exn = if not blocking then (fun () -> raise (NotReady name)), ignore else let lock = Mutex.create () in let cond = Condition.create () in - (fun () -> Mutex.lock lock; Condition.wait cond lock; Mutex.unlock lock), - (fun () -> Mutex.lock lock; Condition.broadcast cond; Mutex.unlock lock) in + (fun () -> CThread.with_lock lock ~scope:(fun () -> Condition.wait cond lock)), + (fun () -> CThread.with_lock lock ~scope:(fun () -> Condition.broadcast cond)) in let ck = create ~name ~fix_exn (Delegated wait) in ck, assignment signal ck diff --git a/lib/pp.mli b/lib/pp.mli index b3c2301d34..865f97166f 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -171,7 +171,7 @@ val prvecti_with_sep : val pr_enum : ('a -> t) -> 'a list -> t (** [pr_enum pr [a ; b ; ... ; c]] outputs - [pr a ++ str "," ++ pr b ++ str "," ++ ... ++ str "and" ++ pr c]. *) + [pr a ++ str "," ++ spc () ++ pr b ++ str "," ++ spc () ++ ... ++ str "and" ++ spc () ++ pr c]. *) val pr_sequence : ('a -> t) -> 'a list -> t (** Sequence of objects separated by space (unless an element is empty). *) @@ -188,7 +188,6 @@ val pp_with : Format.formatter -> t -> unit val string_of_ppcmds : t -> string - (** Tag prefix to start a multi-token diff span *) val start_pfx : string diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml index 5e1150146e..9ea751eef9 100644 --- a/lib/remoteCounter.ml +++ b/lib/remoteCounter.ml @@ -28,10 +28,10 @@ let new_counter ~name a ~incr ~build = managers (that are threads) and the main thread, hence the mutex *) if Flags.async_proofs_is_worker () then CErrors.anomaly(Pp.str"Slave processes must install remote counters."); - Mutex.lock m; let x = f () in Mutex.unlock m; + let x = CThread.with_lock m ~scope:f in build x in let mk_thsafe_remote_getter f () = - Mutex.lock m; let x = f () in Mutex.unlock m; x in + CThread.with_lock m ~scope:f in let getter = ref(mk_thsafe_local_getter (fun () -> !data := incr !!data; !!data)) in let installer f = if not (Flags.async_proofs_is_worker ()) then |