aboutsummaryrefslogtreecommitdiff
path: root/lib/control.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2021-01-14 19:12:11 +0100
committerPierre-Marie Pédrot2021-01-14 19:12:11 +0100
commiteb25e63d58555a67b74a046b8bdf2ab6252164c0 (patch)
treeb3deef1089255b400e66cb540c315d629aff4108 /lib/control.ml
parentb8a3ebaa9695596f062298f5913ae4f4debb0124 (diff)
parent00a09f2cc4a8f4b6baeca0a474e5ab4062ff0f97 (diff)
Merge PR #13378: Add support for high resolution timeout functions
Ack-by: SkySkimmer Ack-by: ejgallego Reviewed-by: ppedrot
Diffstat (limited to 'lib/control.ml')
-rw-r--r--lib/control.ml11
1 files changed, 6 insertions, 5 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 }