diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml index 699745967d929230091a915a67daa2544e1a648b..9c2d3d155bb6a5ade2dae74e883f651a2a3daf14 100644 --- a/src/kernel_services/plugin_entry_points/db.ml +++ b/src/kernel_services/plugin_entry_points/db.ml @@ -1062,9 +1062,63 @@ end (** {2 GUI} *) (* ************************************************************************* *) -let progress = ref (fun () -> ()) +type daemon = { + trigger : unit -> unit ; + debounced : float ; (* in ms *) + mutable next_at : float ; (* next time *) +} + +let pending = ref [] +let daemons = ref [] + +let once trigger = pending := trigger :: !pending + +let on_progress ?(debounced=0) trigger = + let d = { + trigger ; + debounced = float debounced /. 1000.0 ; + next_at = 0.0 ; + } in + daemons := List.append !daemons [d] ; d + +let off_progress d = + daemons := List.filter (fun d0 -> d != d0) !daemons + +let with_progress ?debounced trigger job data = + let d = on_progress ?debounced trigger in + try + let res = job data in + off_progress d ; trigger () ; res + with exn -> + off_progress d ; trigger () ; raise exn + +let yield () = + let jobs = List.rev !pending in + pending := [] ; + List.iter (fun f -> f()) jobs ; + let t = Unix.gettimeofday () in + List.iter (fun d -> + if t > d.next_at then + begin + d.next_at <- t +. d.debounced ; + d.trigger () ; + end + ) !daemons + +let flush () = + List.iter (fun d -> d.next_at <- 0.0) !daemons ; + yield () + +(* +let progress = ref (Kernel.deprecated "!Db.progress()" ~now:"Db.yield()" yield) +*) + +let progress = ref yield exception Cancel +let cancel () = raise Cancel + +(* ************************************************************************* *) (* Local Variables: diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli index b37707a8ae7b1d07f2a3d5ee08266868707eb9c0..196f694814c7074a821cce77c9b2e4c325949ad5 100644 --- a/src/kernel_services/plugin_entry_points/db.mli +++ b/src/kernel_services/plugin_entry_points/db.mli @@ -1339,6 +1339,40 @@ module Derefs : INOUT with type t = Locations.Zone.t @plugin development guide *) val progress: (unit -> unit) ref +(** Registered daemon on progress. *) +type daemon + +(** + Register a new daemon to be executed on [Db.yield()]. + When specified, two succcessive calls to the daemon will be + separated by at least [~debounced] milliseconds (default is 0ms). +*) +val on_progress : ?debounced:int -> (unit -> unit) -> daemon + +(** Un-register the daemon. *) +val off_progress : daemon -> unit + +(** Trigger all daemons immediately. *) +val flush : unit -> unit + +(** Trigger all registered daemons (debounced). *) +val yield : unit -> unit + +(** Trigger a callback once on next [yield()]. *) +val once : (unit -> unit) -> unit + +(** Raises [Cancel] exception *) +val cancel : unit -> unit + +(** + Execute the given job with a temporary registered (debounced) daemon. + Details: [with_progress trigger job data] runs [job data] and returns its + result, with [trigger] registered as a temporary (debounced) daemon. + The daemon is finally flushed and un-registered at the end + of the computation, and any exception is re-raised. +*) +val with_progress : ?debounced:int -> (unit -> unit) -> ('a -> 'b) -> 'a -> 'b + (** This exception may be raised by {!progress} to interrupt computations. *) exception Cancel