src/Pure/Concurrent/timeout.ML
author wenzelm
Sat Apr 02 23:29:05 2016 +0200 (2016-04-02 ago)
changeset 62826 eb94e570c1a4
parent 62519 a564458f94db
child 62923 3a122e1e352a
permissions -rw-r--r--
prefer infix operations;
     1 (*  Title:      Pure/Concurrent/timeout.ML
     2     Author:     Makarius
     3 
     4 Execution with (relative) timeout.
     5 *)
     6 
     7 signature TIMEOUT =
     8 sig
     9   exception TIMEOUT of Time.time
    10   val apply: Time.time -> ('a -> 'b) -> 'a -> 'b
    11   val print: Time.time -> string
    12 end;
    13 
    14 structure Timeout: TIMEOUT =
    15 struct
    16 
    17 exception TIMEOUT of Time.time;
    18 
    19 fun apply timeout f x =
    20   Multithreading.with_attributes Multithreading.no_interrupts (fn orig_atts =>
    21     let
    22       val self = Thread.self ();
    23       val start = Time.now ();
    24 
    25       val request =
    26         Event_Timer.request (start + timeout)
    27           (fn () => Standard_Thread.interrupt_unsynchronized self);
    28       val result =
    29         Exn.capture (fn () => Multithreading.with_attributes orig_atts (fn _ => f x)) ();
    30 
    31       val stop = Time.now ();
    32       val was_timeout = not (Event_Timer.cancel request);
    33       val test = Exn.capture Multithreading.interrupted ();
    34     in
    35       if was_timeout andalso (Exn.is_interrupt_exn result orelse Exn.is_interrupt_exn test)
    36       then raise TIMEOUT (stop - start)
    37       else (Exn.release test; Exn.release result)
    38     end);
    39 
    40 fun print t = "Timeout after " ^ Time.toString t ^ "s";
    41 
    42 end;