From 5e34b11f4326c133b8af0ade8ccca3e805d9b211 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 28 Jan 2020 10:11:13 +0100
Subject: [PATCH] [db] enhanced doc
---
.gitignore | 2 +-
src/kernel_services/plugin_entry_points/db.mli | 15 +++++++++++++++
2 files changed, 16 insertions(+), 1 deletion(-)
diff --git a/.gitignore b/.gitignore
index 6e056235f64..0a653f944d8 100644
--- a/.gitignore
+++ b/.gitignore
@@ -99,8 +99,8 @@ autom4te.cache
/doc/code/print_api/dynamic_plugins.mli
/doc/code/print_api/_build/
+/doc/code/builtin
/doc/code/studia
-
/doc/code/qed
/doc/code/wp
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 1d56b3e036f..4dc4801d439 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -1375,6 +1375,21 @@ val cancel : unit -> unit
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.
+
+
+ Illustrative example, where [...] is the debounced time:
+ {[
+ job data : |<-------------------------------------------------->|<daemon removed>
+ yields : x x x x x x x x xxx xxx
+ trigger : |.......... |.......... |.......... |........|..
+ delayed : !
+ notes : (1) (2) (3) (4)
+ ]}
+
+ 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