diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/control.ml | 11 | ||||
| -rw-r--r-- | lib/control.mli | 4 |
2 files changed, 8 insertions, 7 deletions
diff --git a/lib/control.ml b/lib/control.ml index 7da95ff3dd..ea94bda064 100644 --- a/lib/control.ml +++ b/lib/control.ml @@ -30,11 +30,12 @@ let check_for_interrupt () = (** This function does not work on windows, sigh... *) let unix_timeout n f x = + let open Unix in let timeout_handler _ = raise Timeout in let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in - let _ = Unix.alarm n in + let _ = setitimer ITIMER_REAL {it_interval = 0.; it_value = n} in let restore_timeout () = - let _ = Unix.alarm 0 in + let _ = setitimer ITIMER_REAL { it_interval = 0.; it_value = 0. } in Sys.set_signal Sys.sigalrm psh in try @@ -52,7 +53,7 @@ let windows_timeout n f x = let thread init = while not !killed do let cur = Unix.gettimeofday () in - if float_of_int n <= cur -. init then begin + if n <= cur -. init then begin interrupt := true; exited := true; Thread.exit () @@ -68,7 +69,7 @@ let windows_timeout n f x = let cur = Unix.gettimeofday () in (* The thread did not interrupt, but the computation took longer than expected. *) - let () = if float_of_int n <= cur -. init then begin + let () = if n <= cur -. init then begin exited := true; raise Sys.Break end in @@ -83,7 +84,7 @@ let windows_timeout n f x = let () = killed := true in Exninfo.iraise e -type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> 'b option } +type timeout = { timeout : 'a 'b. float -> ('a -> 'b) -> 'a -> 'b option } let timeout_fun = match Sys.os_type with | "Unix" | "Cygwin" -> { timeout = unix_timeout } diff --git a/lib/control.mli b/lib/control.mli index 9465d8f0d5..f992d8e8d0 100644 --- a/lib/control.mli +++ b/lib/control.mli @@ -24,13 +24,13 @@ 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 -> ('a -> 'b) -> 'a -> 'b option +val timeout : float -> ('a -> 'b) -> 'a -> 'b option (** [timeout n f x] tries to compute [Some (f x)], and if it fails to do so before [n] seconds, returns [None] instead. *) (** Set a particular timeout function; warning, this is an internal API and it is scheduled to go away. *) -type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> 'b option } +type timeout = { timeout : 'a 'b. float -> ('a -> 'b) -> 'a -> 'b option } val set_timeout : timeout -> unit (** [protect_sigalrm f x] computes [f x], but if SIGALRM is received during that |