diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml index f89793e2ca54c929d86673fdade878cb9bdb676b..8824f51b8b9c3aaaf4878bce0334ccd62b0e5f47 100644 --- a/src/kernel_services/plugin_entry_points/db.ml +++ b/src/kernel_services/plugin_entry_points/db.ml @@ -1072,11 +1072,8 @@ type daemon = { (* ---- Registry ---- *) -let pending = ref [] let daemons = ref [] -let once trigger = pending := trigger :: !pending - let on_progress ?(debounced=0) ?on_delayed trigger = let d = { trigger ; @@ -1093,7 +1090,6 @@ let off_progress d = (* ---- Canceling ---- *) exception Cancel -let cancel () = raise Cancel (* ---- Processing ---- *) @@ -1113,20 +1109,15 @@ let with_progress ?debounced ?on_delayed trigger job data = (* ---- Yielding ---- *) -let yield_once () = - match !pending with - | [] -> () - | rjobs -> - pending := [] ; - List.iter (fun f -> f()) (List.rev rjobs) +let canceled = ref false +let cancel () = canceled := true -let yield_daemons () = +let yield () = match !daemons with | [] -> () | ds -> begin let t = Unix.gettimeofday () in - let canceled = ref false in List.iter (fun d -> if t > d.next_at then @@ -1151,13 +1142,9 @@ let yield_daemons () = warn (int_of_float (time_since_last_yield *. 1000.0)) ; d.last_yield_at <- t) ds; - if !canceled then raise Cancel + if !canceled then ( canceled := false ; raise Cancel ) end -let yield () = - yield_daemons () ; - yield_once () - let flush () = List.iter (fun d -> d.next_at <- 0.0) !daemons ; yield () diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli index 2b27d5433eed63ccf30f15b4c93baa105d76f310..407b37ea8f33d57ebc277e4c8fdf487f4b7e5a95 100644 --- a/src/kernel_services/plugin_entry_points/db.mli +++ b/src/kernel_services/plugin_entry_points/db.mli @@ -1363,10 +1363,8 @@ 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 - -(** @raise [Cancel] exception. *) +(** Interrupt the currently running job. + The next call to [Db.yield()] will raise a [Cancel] exception. *) val cancel : unit -> unit (** diff --git a/src/plugins/gui/analyses_manager.ml b/src/plugins/gui/analyses_manager.ml index 87b43c2355fb6170fa1dde032fc8750389450861..9d3dee429ad0615e9314a62c1629477c460a9fe2 100644 --- a/src/plugins/gui/analyses_manager.ml +++ b/src/plugins/gui/analyses_manager.ml @@ -57,7 +57,6 @@ let run_module = let insert (main_ui: Design.main_window_extension_points) = let menu_manager = main_ui#menu_manager () in - let stop () = Db.once Db.cancel in let stop_sensitive = ref false (* can the stop button be clicked? *) in let default_analyses_items = menu_manager#add_plugin @@ -69,7 +68,7 @@ let insert (main_ui: Design.main_window_extension_points) = (Menu_manager.Unit_callback (fun () -> run_module main_ui)); Menu_manager.toolbar ~sensitive:(fun () -> !stop_sensitive) ~icon:`STOP ~label:"Stop" ~tooltip:"Stop currently running analyses" - (Menu_manager.Unit_callback stop) + (Menu_manager.Unit_callback Db.cancel) ] in default_analyses_items.(0)#add_accelerator `CONTROL 'r';