diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-11-27 16:48:39 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-11-27 16:48:39 +0100 |
commit | 4bf305af7e4688b96ec6f407b2a6f4e7e9d7a4a5 (patch) | |
tree | 5d2534ccc35ef94aa34ccd5d96064adb92955a04 /lib | |
parent | 201b6592f7a416c5f5b42f001fc7d629951aa90e (diff) | |
parent | aa560c640eb3f1148c87c4343900138845729105 (diff) |
Merge PR #6241: [lib] Generalize Control.timeout type.
Diffstat (limited to 'lib')
-rw-r--r-- | lib/control.ml | 18 | ||||
-rw-r--r-- | lib/control.mli | 11 |
2 files changed, 11 insertions, 18 deletions
diff --git a/lib/control.ml b/lib/control.ml index f5d7df204..d936d7557 100644 --- a/lib/control.ml +++ b/lib/control.ml @@ -26,7 +26,7 @@ let check_for_interrupt () = end (** This function does not work on windows, sigh... *) -let unix_timeout n f e = +let unix_timeout n f x e = let timeout_handler _ = raise e in let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in let _ = Unix.alarm n in @@ -35,7 +35,7 @@ let unix_timeout n f e = Sys.set_signal Sys.sigalrm psh in try - let res = f () in + let res = f x in restore_timeout (); res with e -> @@ -43,7 +43,7 @@ let unix_timeout n f e = restore_timeout (); Exninfo.iraise e -let windows_timeout n f e = +let windows_timeout n f x e = let killed = ref false in let exited = ref false in let thread init = @@ -60,7 +60,7 @@ let windows_timeout n f e = let init = Unix.gettimeofday () in let _id = Thread.create thread init in try - let res = f () in + let res = f x in let () = killed := true in let cur = Unix.gettimeofday () in (** The thread did not interrupt, but the computation took longer than @@ -80,12 +80,10 @@ let windows_timeout n f e = let e = Backtrace.add_backtrace e in Exninfo.iraise e -type timeout = { timeout : 'a. int -> (unit -> 'a) -> exn -> 'a } +type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> exn -> 'b } let timeout_fun = match Sys.os_type with -| "Unix" | "Cygwin" -> ref { timeout = unix_timeout } -| _ -> ref { timeout = windows_timeout } +| "Unix" | "Cygwin" -> { timeout = unix_timeout } +| _ -> { timeout = windows_timeout } -let set_timeout f = timeout_fun := f - -let timeout n f e = !timeout_fun.timeout n f e +let timeout n f e = timeout_fun.timeout n f e diff --git a/lib/control.mli b/lib/control.mli index 337cdf67b..f6c63ffb3 100644 --- a/lib/control.mli +++ b/lib/control.mli @@ -16,11 +16,6 @@ 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. *) +val timeout : int -> ('a -> 'b) -> 'a -> exn -> 'b +(** [timeout n f x e] tries to compute [f x], and if it fails to do so + before [n] seconds, it raises [e] instead. *) |