From c12bcc423e45367bbb8c8fd757a5732856c42c78 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Wed, 29 Jan 2020 15:03:12 +0100
Subject: [PATCH] [DB] Daemons are not triggered one last time at the end
It simplifies and is not really needed
---
src/kernel_services/plugin_entry_points/db.ml | 18 +++++-------------
src/kernel_services/plugin_entry_points/db.mli | 5 ++---
2 files changed, 7 insertions(+), 16 deletions(-)
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 965b348aa2a..03651ec435e 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -1104,20 +1104,12 @@ let warn_error exn =
let with_progress ?debounced ?delayed trigger job data =
let d = on_progress ?debounced ?delayed trigger in
- let result = try job data with e ->
- off_progress d ;
- (try trigger () with
- (* re-raise job processing exception in all case *)
- | Cancel ->
- (* job exception is also a canceling action *)
- ()
- | exn ->
- (* job exception is more interesting to re-raise *)
- warn_error exn) ;
- raise e
+ let result =
+ try job data with e ->
+ off_progress d ;
+ raise e
in
- (* final trigger is allowed to cancel any englobing jobs *)
- off_progress d ; trigger () ; result
+ off_progress d ; result
(* ---- Yielding ---- *)
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 4dc4801d439..63cda45fa1f 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -1381,15 +1381,14 @@ val cancel : unit -> unit
{[
job data : |<-------------------------------------------------->|<daemon removed>
yields : x x x x x x x x xxx xxx
- trigger : |.......... |.......... |.......... |........|..
+ trigger : |.......... |.......... |.......... |...........
delayed : !
- notes : (1) (2) (3) (4)
+ notes : (1) (2) (3)
]}
1. First yield, normal trigger
2. Debounced yields leads to this second trigger
3. Delayed warning invoked since there was no yield for more than debounced period
- 4. Final trigger, a bit before the debounced time
*)
val with_progress : ?debounced:int -> ?delayed:(int -> unit) ->
(unit -> unit) -> ('a -> 'b) -> 'a -> 'b
--
GitLab