[kernel] new progress API

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:

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