From e196b694195dfb88ec2b44e83828f6feb1ccf012 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 31 May 2022 16:07:04 +0200
Subject: [PATCH] [Db] generalization of [on|off|with|while]_progress
---
src/kernel_services/plugin_entry_points/db.ml | 39 +++++++-----
.../plugin_entry_points/db.mli | 60 ++++++++-----------
2 files changed, 51 insertions(+), 48 deletions(-)
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 4d69ac1a7f4..a091fe04227 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -930,6 +930,7 @@ end
type daemon = {
trigger : unit -> unit ;
on_delayed : (int -> unit) option ;
+ on_finished : (unit -> unit) option ;
debounced : float ; (* in ms *)
mutable next_at : float ; (* next trigger time *)
mutable last_yield_at : float ; (* last yield time *)
@@ -939,32 +940,33 @@ type daemon = {
let daemons = ref []
-let on_progress ?(debounced=0) ?on_delayed trigger =
+let on_progress ?(debounced=0) ?on_delayed ?on_finished trigger =
let d = {
trigger ;
debounced = float debounced *. 0.001 ;
on_delayed ;
+ on_finished ;
last_yield_at = 0.0 ;
next_at = 0.0 ;
} in
daemons := List.append !daemons [d] ; d
let off_progress d =
- daemons := List.filter (fun d0 -> d != d0) !daemons
-
-(* ---- Canceling ---- *)
-
-exception Cancel
-
-(* ---- Processing ---- *)
+ daemons := List.filter (fun d0 -> d != d0) !daemons ;
+ match d.on_finished with
+ | None -> ()
+ | Some f -> f ()
-let warn_error exn =
- Kernel.failure
- "Unexpected Db.daemon exception:@\n%s"
- (Printexc.to_string exn)
+let while_progress ?debounced ?on_delayed ?on_finished progress =
+ let d : daemon option ref = ref None in
+ let trigger () =
+ if not @@ progress () then
+ Option.iter off_progress !d
+ in
+ d := Some (on_progress ?debounced ?on_delayed ?on_finished trigger)
-let with_progress ?debounced ?on_delayed trigger job data =
- let d = on_progress ?debounced ?on_delayed trigger in
+let with_progress ?debounced ?on_delayed ?on_finished trigger job data =
+ let d = on_progress ?debounced ?on_delayed ?on_finished trigger in
let result =
try job data
with exn ->
@@ -973,11 +975,20 @@ let with_progress ?debounced ?on_delayed trigger job data =
in
off_progress d ; result
+(* ---- Canceling ---- *)
+
+exception Cancel
+
(* ---- Triggering ---- *)
let canceled = ref false
let cancel () = canceled := true
+let warn_error exn =
+ Kernel.failure
+ "Unexpected Db.daemon exception:@\n%s"
+ (Printexc.to_string exn)
+
let fire ~warn_on_delayed ~forced ~time d =
if forced || time > d.next_at then
begin
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 62334a53e2e..2e3d4229914 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -947,56 +947,48 @@ type daemon
daemon to be executed on each {!yield}.
@param debounced the least amount of time between two successive calls to the
daemon, in milliseconds (default is 0ms).
- @param on_delayed the callback invoked as soon as the time since the last
+ @param on_delayed callback is invoked as soon as the time since the last
{!yield} is greater than [debounced] milliseconds (or 100ms at least).
+ @param on_finished callback is invoked when the callback is unregistered.
*)
val on_progress :
- ?debounced:int -> ?on_delayed:(int -> unit) -> (unit -> unit) -> daemon
+ ?debounced:int -> ?on_delayed:(int -> unit) -> ?on_finished:(unit -> unit) ->
+ (unit -> unit) -> daemon
(** Unregister the [daemon]. *)
val off_progress : daemon -> unit
-(** Trigger all daemons immediately. *)
-val flush : unit -> unit
-
-(** Trigger all registered daemons (debounced).
- This function should be called from time to time by all analysers taking
- time. In GUI mode, this will make the interface reactive. *)
-val yield : unit -> unit
-
-(** Interrupt the currently running job at the next call to {!yield} as a
- [Cancel] exception is raised. *)
-val cancel : unit -> unit
+(** [while_progress ?debounced ?on_delayed ?on_finished trigger] is similar to
+ [on_progress] but the daemon is automatically unregistered
+ as soon as [trigger] returns [false].
+ Same optional parameters than [on_progress].
+*)
+val while_progress :
+ ?debounced:int -> ?on_delayed:(int -> unit) -> ?on_finished:(unit -> unit) ->
+ (unit -> bool) -> unit
(**
[with_progress ?debounced ?on_delayed trigger job data] executes the given
[job] on [data] while registering [trigger] as temporary (debounced) daemon.
The daemon is finally unregistered at the end of the computation.
-
- Illustrative example, where [...] is the debounced time:
- {[
- job data : |<-------------------------------------------------->|<daemon removed>
- yields : x x x x x x x x xxx xxx
- trigger : |.......... |.......... |.......... |.........
- delayed : !
- notes : (1) (2) (3)
- ]}
-
- + First yield, normal trigger.
- + Debounced yields leads to this second trigger.
- + Delayed warning invoked since there was no yield for more than debounced period.
-
- Raises every exception raised during the execution of [job] on [data].
-
- @param debounced the least amount of time, in milliseconds, between two
- successive calls to the daemon (default is 0ms).
- @param on_delayed the callback invoked as soon as the time since the last
- [yield] is greater than [debounced] milliseconds (or 100ms at least).
+ Same optional parameters than [on_progress].
*)
val with_progress :
- ?debounced:int -> ?on_delayed:(int -> unit) ->
+ ?debounced:int -> ?on_delayed:(int -> unit) -> ?on_finished:(unit -> unit) ->
(unit -> unit) -> ('a -> 'b) -> 'a -> 'b
+(** Trigger all daemons immediately. *)
+val flush : unit -> unit
+
+(** Trigger all registered daemons (debounced).
+ This function should be called from time to time by all analysers taking
+ time. In GUI or Server mode, this will make the clients responsive. *)
+val yield : unit -> unit
+
+(** Interrupt the currently running job: the next call to {!yield}
+ will raise a [Cancel] exception. *)
+val cancel : unit -> unit
+
(**
Pauses the currently running process for the specified time, in milliseconds.
Registered daemons, if any, will be regularly triggered during this waiting
--
GitLab