Future: ported to Ephemeron + exception enhancing

A future always carries a fix_exn with it: a function that enriches
an exception with the state in which the error occurs and also a safe
state close to it where one could backtrack.

A future can be in two states: Ongoing or Finished.
The latter state is obtained by Future.join and after that the future
can be safely marshalled.
An Ongoing future can be marshalled, but its value is lost.  This makes
it possible to send the environment to a slave process without
pre-processing it to drop all unfinished proofs (they are dropped
automatically in some sense).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16892 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 11 insertions, 9 deletions

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 81bfcaccee..08eaa30f50 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -277,18 +277,18 @@ let close_proof ~now fpl =
     List.iter (fun x -> ignore(Future.compute x.Entries.const_entry_body)) entries;
   (pid, (entries, compute_guard, strength, hook))
 
-let return_proof ~fix_exn =
+let return_proof () =
   let { proof } = cur_pstate () in
   let initial_goals = Proof.initial_goals proof in
   let evd =
    try Proof.return proof with
    | Proof.UnfinishedProof ->
-       raise (fix_exn(Errors.UserError("last tactic before Qed",
-         str"Attempt to save an incomplete proof")))
+       raise (Errors.UserError("last tactic before Qed",
+         str"Attempt to save an incomplete proof"))
    | Proof.HasUnresolvedEvar ->
-       raise (fix_exn(Errors.UserError("last tactic before Qed",
+       raise (Errors.UserError("last tactic before Qed",
          str"Attempt to save a proof with existential " ++
-         str"variables still non-instantiated")))
+         str"variables still non-instantiated"))
   in
   let eff = Evd.eval_side_effects evd in
   (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
@@ -297,8 +297,8 @@ let return_proof ~fix_exn =
   List.map (fun (c, _) -> (Evarutil.nf_evar evd c, eff)) initial_goals
 
 let close_future_proof proof = close_proof ~now:false proof
-let close_proof () =
-  close_proof ~now:true (Future.from_here (return_proof ~fix_exn:(fun x -> x)))
+let close_proof fix_exn =
+  close_proof ~now:true (Future.from_here ~fix_exn (return_proof ()))
 
 (**********************************************************)
 (*                                                        *)
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 5922075ec7..9d7407010c 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -64,12 +64,14 @@ type closed_proof =
   (Entries.definition_entry list * lemma_possible_guards *
     Decl_kinds.goal_kind * unit Tacexpr.declaration_hook)
 
-val close_proof : unit -> closed_proof
+(* Takes a function to add to the exceptions data relative to the
+   state in which the proof was built *)
+val close_proof : (exn -> exn) -> closed_proof
 
 (* Intermediate step necessary to delegate the future.
  * Both access the current proof state. The formes is supposed to be
  * chained with a computation that completed the proof *)
-val return_proof : fix_exn:(exn -> exn) -> Entries.proof_output list
+val return_proof : unit -> Entries.proof_output list
 val close_future_proof :
   Entries.proof_output list Future.computation -> closed_proof