1(*  Title:      Pure/Concurrent/timeout.ML
2    Author:     Makarius
3
4Execution with (relative) timeout.
5*)
6
7signature TIMEOUT =
8sig
9  exception TIMEOUT of Time.time
10  val apply: Time.time -> ('a -> 'b) -> 'a -> 'b
11end;
12
13structure Timeout: TIMEOUT =
14struct
15
16exception TIMEOUT of Time.time;
17
18fun apply timeout f x =
19  Thread_Attributes.with_attributes Thread_Attributes.no_interrupts (fn orig_atts =>
20    let
21      val self = Thread.self ();
22      val start = Time.now ();
23
24      val request =
25        Event_Timer.request (start + timeout)
26          (fn () => Standard_Thread.interrupt_unsynchronized self);
27      val result =
28        Exn.capture (fn () => Thread_Attributes.with_attributes orig_atts (fn _ => f x)) ();
29
30      val stop = Time.now ();
31      val was_timeout = not (Event_Timer.cancel request);
32      val test = Exn.capture Thread_Attributes.expose_interrupt ();
33    in
34      if was_timeout andalso (Exn.is_interrupt_exn result orelse Exn.is_interrupt_exn test)
35      then raise TIMEOUT (stop - start)
36      else (Exn.release test; Exn.release result)
37    end);
38
39end;
40