diff options
-rw-r--r-- | engine/logic_monad.ml | 2 | ||||
-rw-r--r-- | lib/control.ml | 18 | ||||
-rw-r--r-- | lib/control.mli | 11 | ||||
-rw-r--r-- | vernac/vernacentries.ml | 2 |
4 files changed, 13 insertions, 20 deletions
diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml index bf1b3e0e8..9dc5d473b 100644 --- a/engine/logic_monad.ml +++ b/engine/logic_monad.ml @@ -95,7 +95,7 @@ struct let print_char = fun c -> (); fun () -> print_char c let timeout = fun n t -> (); fun () -> - Control.timeout n t (Exception Timeout) + Control.timeout n t () (Exception Timeout) let make f = (); fun () -> try f () 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. *) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 62c7edb19..9a67aa6dd 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2144,7 +2144,7 @@ let vernac_timeout f = match !current_timeout, !default_timeout with | Some n, _ | None, Some n -> let f () = f (); current_timeout := None in - Control.timeout n f Timeout + Control.timeout n f () Timeout | None, None -> f () let restore_timeout () = current_timeout := None |