diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/future.ml | 7 | ||||
| -rw-r--r-- | lib/future.mli | 12 |
2 files changed, 18 insertions, 1 deletions
diff --git a/lib/future.ml b/lib/future.ml index 77386a1a9f..960363e252 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -91,6 +91,13 @@ let from_val ?(fix_exn=id) v = create fix_exn (Val (v, None)) let from_here ?(fix_exn=id) v = create fix_exn (Val (v, Some (!freeze ()))) let fix_exn_of ck = let _, fix_exn, _ = get ck in fix_exn +type 'a hook = Decl_kinds.locality -> Globnames.global_reference -> 'a +let mk_hook hook = hook +let call_hook fix_exn hook l c = + try hook l c + with e when Errors.noncritical e -> + let e = Errors.push e in + raise (fix_exn e) let default_force () = raise NotReady let assignement ck = fun v -> diff --git a/lib/future.mli b/lib/future.mli index b4eced06a9..41f5e185c9 100644 --- a/lib/future.mli +++ b/lib/future.mli @@ -84,8 +84,18 @@ 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 -(* To get the fix_exn of a computation *) +(* To get the fix_exn of a computation and build a Tacexpr.declaration_hook. + * When a future enters the environment a corresponding hook is run to perform + * some work. If this fails, then its failure has to be annotated with the + * same state id that corresponds to the future computation end. I.e. Qed + * is split into two parts, the lazy one (the future) and the eagher one + * (the hook), both performing some computations for the same state id. *) val fix_exn_of : 'a computation -> fix_exn +type 'a hook +val mk_hook : + (Decl_kinds.locality -> Globnames.global_reference -> 'a) -> 'a hook +val call_hook : + fix_exn -> 'a hook -> Decl_kinds.locality -> Globnames.global_reference -> 'a (* Run remotely, returns the function to assign. Optionally tekes a function that is called when forced. The default one is to raise NotReady. |