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

5 files changed, 67 insertions, 12 deletions

diff --git a/lib/clib.mllib b/lib/clib.mllib
index 1dc540b9a..cd8964f02 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -12,6 +12,7 @@ Option
 Store
 Exninfo
 Backtrace
+Control
 IArray
 IStream
 Pp_control
diff --git a/lib/control.ml b/lib/control.ml
new file mode 100644
index 000000000..9573614fd
--- /dev/null
+++ b/lib/control.ml
@@ -0,0 +1,40 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*s interruption *)
+
+let interrupt = ref false
+
+let check_for_interrupt () =
+  if !interrupt then begin interrupt := false; raise Sys.Break end
+
+(** This function does not work on windows, sigh... *)
+let unix_timeout n f e =
+  let timeout_handler _ = raise e in
+  let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in
+  let _ = Unix.alarm n in
+  let restore_timeout () =
+    let _ = Unix.alarm 0 in
+    Sys.set_signal Sys.sigalrm psh
+  in
+  try
+    let res = f () in
+    restore_timeout ();
+    res
+  with e ->
+    let e = Backtrace.add_backtrace e in
+    restore_timeout ();
+    raise e
+
+type timeout = { timeout : 'a. int -> (unit -> 'a) -> exn -> 'a }
+
+let timeout_fun = ref { timeout = unix_timeout }
+
+let set_timeout f = timeout_fun := f
+
+let timeout n f e = !timeout_fun.timeout n f e
diff --git a/lib/control.mli b/lib/control.mli
new file mode 100644
index 000000000..36c834915
--- /dev/null
+++ b/lib/control.mli
@@ -0,0 +1,26 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Global control of Coq. *)
+
+val interrupt : bool ref
+(** Coq interruption: set the following boolean reference to interrupt Coq
+    (it eventually raises [Break], simulating a Ctrl-C) *)
+
+val check_for_interrupt : unit -> unit
+(** Use this function as a potential yield function. If {!interrupt} has been
+    set, il will raise [Sys.Break]. *)
+
+val timeout : int -> (unit -> 'a) -> exn -> 'a
+(** [timeout n f e] tries to compute [f], and if it fails to do so before [n]
+    seconds, it raises [e] instead. *)
+
+type timeout = { timeout : 'a. int -> (unit -> 'a) -> exn -> 'a }
+
+val set_timeout : timeout -> unit
+(** Set a particular timeout function. *)
diff --git a/lib/util.ml b/lib/util.ml
index 9ade75147..16b5f4615 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -124,9 +124,3 @@ let delayed_force f = f ()
 
 type ('a, 'b) union = ('a, 'b) CSig.union = Inl of 'a | Inr of 'b
 type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a
-
-(*s interruption *)
-
-let interrupt = ref false
-let check_for_interrupt () =
-  if !interrupt then begin interrupt := false; raise Sys.Break end
diff --git a/lib/util.mli b/lib/util.mli
index d3e3432a3..fd766a30f 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -103,9 +103,3 @@ type ('a, 'b) union = ('a, 'b) CSig.union = Inl of 'a | Inr of 'b
 type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a
 (** Used for browsable-until structures. *)
 
-(** {6 ... } *)
-(** Coq interruption: set the following boolean reference to interrupt Coq
-    (it eventually raises [Break], simulating a Ctrl-C) *)
-
-val interrupt : bool ref
-val check_for_interrupt : unit -> unit