diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-06-07 00:28:29 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-06-07 01:20:25 +0200 |
commit | 24a0df63c1844c6f2c69f9644a3059d668fd1e6f (patch) | |
tree | 950372175994d0f5211b984a63bfee039cac4ebe /lib/control.ml | |
parent | e6a7182526a47f4010274128c30407ed57e51339 (diff) |
Adding a new Control file centralizing the control options of Coq.
Diffstat (limited to 'lib/control.ml')
-rw-r--r-- | lib/control.ml | 40 |
1 files changed, 40 insertions, 0 deletions
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 |