diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml index 8824f51b8b9c3aaaf4878bce0334ccd62b0e5f47..2f429dcb0d796213c0bafbaf24563148686abeac 100644 --- a/src/kernel_services/plugin_entry_points/db.ml +++ b/src/kernel_services/plugin_entry_points/db.ml @@ -1077,7 +1077,7 @@ let daemons = ref [] let on_progress ?(debounced=0) ?on_delayed trigger = let d = { trigger ; - debounced = float debounced /. 1000.0 ; + debounced = float debounced *. 0.001 ; on_delayed ; last_yield_at = 0.0 ; next_at = 0.0 ; @@ -1107,47 +1107,85 @@ let with_progress ?debounced ?on_delayed trigger job data = in off_progress d ; result -(* ---- Yielding ---- *) +(* ---- Triggering ---- *) let canceled = ref false let cancel () = canceled := true -let yield () = +let fire ~delayed ~forced ~time d = + if forced || time > d.next_at then + begin + try + d.next_at <- time +. d.debounced ; + d.trigger () ; + with + | Cancel -> canceled := true + | exn -> warn_error exn ; raise exn + end ; + match d.on_delayed with + | None -> () + | Some warn -> + if delayed && 0.0 < d.last_yield_at then + begin + let time_since_last_yield = time -. d.last_yield_at in + let delay = if d.debounced > 0.0 then d.debounced else 0.1 in + if time_since_last_yield > delay then + warn (int_of_float (time_since_last_yield *. 1000.0)) ; + end ; + d.last_yield_at <- time + +let raise_if_canceled () = + if !canceled then ( canceled := false ; raise Cancel ) + +(* ---- Yielding ---- *) + +let trigger ~delayed ~forced () = match !daemons with | [] -> () | ds -> begin - let t = Unix.gettimeofday () in - List.iter - (fun d -> - if t > d.next_at then - begin - try - d.next_at <- t +. d.debounced ; - d.trigger () ; - with - | Cancel -> canceled := true - | exn -> warn_error exn ; raise exn - end ; - match d.on_delayed with - | None -> - () - | Some _ when d.last_yield_at = 0. -> - (* first yield *) - d.last_yield_at <- t - | Some warn -> - let time_since_last_yield = t -. d.last_yield_at in - let delay = if d.debounced > 0.0 then d.debounced else 0.1 in - if time_since_last_yield > delay then - warn (int_of_float (time_since_last_yield *. 1000.0)) ; - d.last_yield_at <- t) - ds; - if !canceled then ( canceled := false ; raise Cancel ) + let time = Unix.gettimeofday () in + List.iter (fire ~delayed ~forced ~time) ds ; + raise_if_canceled () ; end -let flush () = - List.iter (fun d -> d.next_at <- 0.0) !daemons ; - yield () +let yield = trigger ~delayed:true ~forced:false +let flush = trigger ~delayed:false ~forced:true + +(* ---- Sleeping ---- *) + +let rec gcd a b = if b = 0 then a else gcd b (a mod b) + +(* n=0 means no periodic daemons (yet) *) +let merge_period n { debounced = p } = + if p > 0.0 then gcd (int_of_float (p *. 1000.0)) n else n + +let sleep ms = + if ms > 0 then + let delta = float ms *. 0.001 in + let period = List.fold_left merge_period 0 !daemons in + if period = 0 then + begin + Unix.sleepf delta ; + trigger ~delayed:false ~forced:false () + end + else + let delay = float period *. 0.001 in + let finished_at = Unix.gettimeofday () +. delta in + let rec wait_and_trigger () = + begin + Unix.sleepf delay ; + let time = Unix.gettimeofday () in + List.iter (fire ~delayed:false ~forced:false ~time) !daemons ; + raise_if_canceled () ; + if time < finished_at then + if time +. delay > finished_at then + Unix.sleepf (finished_at -. time) + else wait_and_trigger () + end + in wait_and_trigger () + +(* ---- Deprecated old API ---- *) let progress = ref (Kernel.deprecated "!Db.progress()" ~now:"Db.yield()" yield) diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli index 02f3e32ba3d2f081f9416489228b92ec387cb6e0..b851a5819c39b8a531d8389861a3565c4fb94380 100644 --- a/src/kernel_services/plugin_entry_points/db.mli +++ b/src/kernel_services/plugin_entry_points/db.mli @@ -1399,6 +1399,14 @@ val with_progress : ?debounced:int -> ?on_delayed:(int -> unit) -> (unit -> unit) -> ('a -> 'b) -> 'a -> 'b + +(** + Pauses the currently running process for the specified time, in milli-seconds. + Registered daemons, if any, will be regularily triggered during this waiting + time at a reasonnable period with respect to their debouncing constraints. +*) +val sleep : int -> unit + (** This exception may be raised by {!progress} to interrupt computations. *) exception Cancel