diff options
Diffstat (limited to 'lib/control.ml')
| -rw-r--r-- | lib/control.ml | 24 |
1 files changed, 13 insertions, 11 deletions
diff --git a/lib/control.ml b/lib/control.ml index 95ea3935a7..7da95ff3dd 100644 --- a/lib/control.ml +++ b/lib/control.ml @@ -16,6 +16,8 @@ let steps = ref 0 let enable_thread_delay = ref false +exception Timeout + let check_for_interrupt () = if !interrupt then begin interrupt := false; raise Sys.Break end; if !enable_thread_delay then begin @@ -27,8 +29,8 @@ let check_for_interrupt () = end (** This function does not work on windows, sigh... *) -let unix_timeout n f x e = - let timeout_handler _ = raise e in +let unix_timeout n f x = + let timeout_handler _ = raise Timeout in let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in let _ = Unix.alarm n in let restore_timeout () = @@ -38,13 +40,13 @@ let unix_timeout n f x e = try let res = f x in restore_timeout (); - res - with e -> - let e = Exninfo.capture e in + Some res + with Timeout -> restore_timeout (); - Exninfo.iraise e + None + -let windows_timeout n f x e = +let windows_timeout n f x = let killed = ref false in let exited = ref false in let thread init = @@ -70,18 +72,18 @@ let windows_timeout n f x e = exited := true; raise Sys.Break end in - res + Some res with | Sys.Break -> (* Just in case, it could be a regular Ctrl+C *) if not !exited then begin killed := true; raise Sys.Break end - else raise e + else None | e -> let e = Exninfo.capture e in let () = killed := true in Exninfo.iraise e -type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> exn -> 'b } +type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> 'b option } let timeout_fun = match Sys.os_type with | "Unix" | "Cygwin" -> { timeout = unix_timeout } @@ -90,7 +92,7 @@ let timeout_fun = match Sys.os_type with let timeout_fun_ref = ref timeout_fun let set_timeout f = timeout_fun_ref := f -let timeout n f e = !timeout_fun_ref.timeout n f e +let timeout n f = !timeout_fun_ref.timeout n f let protect_sigalrm f x = let timed_out = ref false in |
