From a5ebab4f0cd762904055a69b20e6217d08f46637 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 20 Dec 2013 12:23:30 +0100
Subject: Future: allow custom action when a delegated future is forced

The default action is to raise NotReady, but one may want to
make the action "blocking" but successful.  Using this device
all delayed proofs can be "delegated".  If there are slaves, they
will eventually pick up the task.  If there are no slaves, then
the future can behave like a regular, non delegated, lazy computation.
---
 lib/future.mli | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'lib/future.mli')

diff --git a/lib/future.mli b/lib/future.mli
index 1a1648ff1f..4f27767ba4 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -74,9 +74,12 @@ val from_val : ?fix_exn:fix_exn -> 'a -> 'a computation
    the value is not just the 'a but also the global system state *)
 val from_here : ?fix_exn:fix_exn -> 'a -> 'a computation
 
-(* Run remotely, returns the function to assign *)
+(* Run remotely, returns the function to assign.  Optionally tekes a function
+   that is called when forced.  The default one is to raise NotReady *)
 type 'a assignement = [ `Val of 'a | `Exn of exn | `Comp of 'a computation]
-val create_delegate : fix_exn -> 'a computation * ('a assignement -> unit)
+val create_delegate :
+  ?force:(unit -> 'a assignement) ->
+  fix_exn -> 'a computation * ('a assignement -> unit)
 
 (* Given a computation that is_exn, replace it by another one *)
 val replace : 'a computation -> 'a computation -> unit
-- 
cgit v1.2.3