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