From 289b2b9a1c3d3ebc3c1975663d16c04e88b6329b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 2 Jun 2014 10:52:31 +0200 Subject: Enforce a correct exception handling in declaration_hooks This should finally get rid of the following class of bugs: Qed fails, STM undoes to the beginning of the proof because the exception is not annotated with the correct state, PG gets out of sync because errors always refer to the last command in PGIP. --- lib/future.mli | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) (limited to 'lib/future.mli') diff --git a/lib/future.mli b/lib/future.mli index b4eced06a..41f5e185c 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. -- cgit v1.2.3