Adding a new Control file centralizing the control options of Coq.

2 files changed, 6 insertions, 21 deletions

diff --git a/proofs/proofview_gen.ml b/proofs/proofview_gen.ml
index a686c528c3..cb195c5e8a 100644
--- a/proofs/proofview_gen.ml
+++ b/proofs/proofview_gen.ml
@@ -75,24 +75,9 @@ module IOBase =
   (** val timeout : int -> 'a1 coq_T -> 'a1 coq_T **)
   
   let timeout = fun n t -> (); fun () ->
-    let timeout_handler _ = Pervasives.raise (Proof_errors.Exception Proof_errors.Timeout) in
-    let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in
-    Pervasives.ignore (Unix.alarm n);
-    let restore_timeout () =
-      Pervasives.ignore (Unix.alarm 0);
-      Sys.set_signal Sys.sigalrm psh
-    in
-    try
-      let res = t () in
-      restore_timeout ();
-      res
-    with
-    | e ->
-      let e = Errors.push e in
-      restore_timeout ();
-      Pervasives.raise e
- 
- end
+    Control.timeout n t (Proof_errors.Exception Proof_errors.Timeout)
+
+end
 
 type proofview = { solution : Evd.evar_map; comb : Goal.goal list }
 
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 157faae3dd..f0e8bf3ec7 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -44,7 +44,7 @@ let unpackage glsig = (ref (glsig.sigma)), glsig.it
 let repackage r v = {it = v; sigma = !r; }
 
 let apply_sig_tac r tac g =
-  check_for_interrupt (); (* Breakpoint *)
+  Control.check_for_interrupt (); (* Breakpoint *)
   let glsigma = tac (repackage r g) in
   r := glsigma.sigma;
   glsigma.it
@@ -219,10 +219,10 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
 
 
 let catch_failerror e =
-  if catchable_exception e then check_for_interrupt ()
+  if catchable_exception e then Control.check_for_interrupt ()
   else match e with
   | FailError (0,_) ->
-      check_for_interrupt ()
+      Control.check_for_interrupt ()
   | FailError (lvl,s) ->
     raise (Exninfo.copy e (FailError (lvl - 1, s)))
   | e -> raise e