From 58f59b29ed35860142e39049ed9d09b2e71f86ab Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Wed, 29 Jan 2020 16:44:50 +0100
Subject: [PATCH] [db] Rework style and especially the doc.
---
src/kernel_services/plugin_entry_points/db.ml | 66 ++++++++++---------
.../plugin_entry_points/db.mli | 41 ++++++------
src/plugins/server/main.ml | 4 +-
3 files changed, 59 insertions(+), 52 deletions(-)
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 3db4d315aa2..f89793e2ca5 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -1064,7 +1064,7 @@ end
type daemon = {
trigger : unit -> unit ;
- delayed : (int -> unit) option ;
+ on_delayed : (int -> unit) option ;
debounced : float ; (* in ms *)
mutable next_at : float ; (* next trigger time *)
mutable last_yield_at : float ; (* last yield time *)
@@ -1077,11 +1077,11 @@ let daemons = ref []
let once trigger = pending := trigger :: !pending
-let on_progress ?(debounced=0) ?delayed trigger =
+let on_progress ?(debounced=0) ?on_delayed trigger =
let d = {
trigger ;
debounced = float debounced /. 1000.0 ;
- delayed ;
+ on_delayed ;
last_yield_at = 0.0 ;
next_at = 0.0 ;
} in
@@ -1102,8 +1102,8 @@ let warn_error exn =
"Unexpected Db.daemon exception:@\n%s"
(Printexc.to_string exn)
-let with_progress ?debounced ?delayed trigger job data =
- let d = on_progress ?debounced ?delayed trigger in
+let with_progress ?debounced ?on_delayed trigger job data =
+ let d = on_progress ?debounced ?on_delayed trigger in
let result =
try job data with e ->
off_progress d ;
@@ -1124,35 +1124,39 @@ let yield_daemons () =
match !daemons with
| [] -> ()
| ds ->
- let t = Unix.gettimeofday () in
- let canceled = ref false in
- List.iter
- begin fun d ->
- let delta = d.debounced in
- if t > d.next_at then
- begin
- try
- d.next_at <- t +. delta ;
- d.trigger () ;
- with Cancel -> canceled := true
+ begin
+ let t = Unix.gettimeofday () in
+ let canceled = ref false 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.delayed with
- | None -> ()
- | Some _ when d.last_yield_at = 0. -> d.last_yield_at <- t (* first yield *)
- | Some warn ->
- let period = t -. d.last_yield_at in
- let delay = if delta > 0.0 then delta else 0.1 in
- if period > delay then warn (int_of_float (period *. 1000.0)) ;
- d.last_yield_at <- t ;
- end ds ;
- if !canceled then raise Cancel
+ 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 raise Cancel
+ end
let yield () =
- begin
- yield_daemons () ;
- yield_once () ;
- end
+ yield_daemons () ;
+ yield_once ()
let flush () =
List.iter (fun d -> d.next_at <- 0.0) !daemons ;
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 63cda45fa1f..2b27d5433ee 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -1343,16 +1343,18 @@ val progress: (unit -> unit) ref
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).
- The [~delayed d] callback is invoked when [Db.yield()] has not been called
- since a delay [d] greater than [~debounced] or 100ms.
+
+ [on_progress ?debounced ?on_delayed trigger] registers [trigger] as new
+ daemon to be executed on each [yield].
+ @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).
*)
val on_progress :
- ?debounced:int -> ?delayed:(int -> unit) -> (unit -> unit) -> daemon
+ ?debounced:int -> ?on_delayed:(int -> unit) -> (unit -> unit) -> daemon
-(** Un-register the daemon. *)
+(** Unregister the [daemon]. *)
val off_progress : daemon -> unit
(** Trigger all daemons immediately. *)
@@ -1361,27 +1363,27 @@ val flush : unit -> unit
(** Trigger all registered daemons (debounced). *)
val yield : unit -> unit
-(** Trigger a callback once on next [yield()]. *)
+(** Trigger a callback once on next [yield]. *)
val once : (unit -> unit) -> unit
-(** Raises [Cancel] exception *)
+(** @raise [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.
- The callback [~on_mute d] is triggered when the deamon has not been yielded
- for a period [d] longer than [~debounce] or 100ms by default.
-
+ [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.
+ @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).
+ @raise every exception raised during the execution of [job] on [data].
Illustrative example, where [...] is the debounced time:
{[
job data : |<-------------------------------------------------->|<daemon removed>
yields : x x x x x x x x xxx xxx
- trigger : |.......... |.......... |.......... |...........
+ trigger : |.......... |.......... |.......... |.........
delayed : !
notes : (1) (2) (3)
]}
@@ -1390,7 +1392,8 @@ val cancel : unit -> unit
2. Debounced yields leads to this second trigger
3. Delayed warning invoked since there was no yield for more than debounced period
*)
-val with_progress : ?debounced:int -> ?delayed:(int -> unit) ->
+val with_progress :
+ ?debounced:int -> ?on_delayed:(int -> unit) ->
(unit -> unit) -> ('a -> 'b) -> 'a -> 'b
(** This exception may be raised by {!progress} to interrupt computations. *)
diff --git a/src/plugins/server/main.ml b/src/plugins/server/main.ml
index f6b94ed2083..c628ffc4c34 100644
--- a/src/plugins/server/main.ml
+++ b/src/plugins/server/main.ml
@@ -145,13 +145,13 @@ let execute exec : _ response =
`Error(exec.id,Printexc.to_string exn)
let execute_debug server yield exec =
- let delayed =
+ let on_delayed =
if Senv.debug_atleast 1 then
(Senv.debug "Trigger %s:%a" exec.request server.pretty exec.id ;
Some (fun delay -> Senv.debug
"No yield since %dms during %s" delay exec.request))
else None
- in Db.with_progress ~debounced:server.yield ?delayed yield execute exec
+ in Db.with_progress ~debounced:server.yield ?on_delayed yield execute exec
let reply_debug server resp =
if Senv.debug_atleast 1 then
--
GitLab