diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml index 965b348aa2afdf050c7a8772b2aa6e075245cc30..03651ec435e779ed0efb39a553d02a2943eebd48 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 4dc4801d439153529e28113c7575eaabeb71230b..63cda45fa1f59caa25273c30dc089c706d9ffdaa 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