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.

2 files changed, 18 insertions, 1 deletions

diff --git a/lib/future.ml b/lib/future.ml
index 77386a1a9..960363e25 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 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.