From 28dc1b1ca8eaaf9d0bc9e8ab2c6ce62e8fc9242a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 27 Jan 2020 14:27:22 +0100
Subject: [PATCH] [kernel] optimise Db.yield a bit
---
src/kernel_services/plugin_entry_points/db.ml | 35 +++++++++++++------
1 file changed, 24 insertions(+), 11 deletions(-)
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index bf1eb6ce502..c98fe4dd36a 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -1092,18 +1092,31 @@ let with_progress ?debounced trigger job data =
with exn ->
off_progress d ; trigger () ; raise exn
+let yield_once () =
+ match !pending with
+ | [] -> ()
+ | rjobs ->
+ pending := [] ;
+ List.iter (fun f -> f()) (List.rev rjobs)
+
+let yield_daemons () =
+ match !daemons with
+ | [] -> ()
+ | ds ->
+ let t = Unix.gettimeofday () in
+ List.iter (fun d ->
+ if t > d.next_at then
+ begin
+ d.next_at <- t +. d.debounced ;
+ d.trigger () ;
+ end
+ ) ds
+
let yield () =
- let jobs = List.rev !pending in
- pending := [] ;
- List.iter (fun f -> f()) jobs ;
- let t = Unix.gettimeofday () in
- List.iter (fun d ->
- if t > d.next_at then
- begin
- d.next_at <- t +. d.debounced ;
- d.trigger () ;
- end
- ) !daemons
+ begin
+ yield_once () ;
+ yield_daemons () ;
+ end
let flush () =
List.iter (fun d -> d.next_at <- 0.0) !daemons ;
--
GitLab