modernized TimeLimit.timeLimit using Event_Timer service -- based on more elementary version 11ae688e4e30;

--- a/src/Pure/Concurrent/time_limit.ML	Fri May 17 17:11:06 2013 +0200
+++ b/src/Pure/Concurrent/time_limit.ML	Fri May 17 17:45:51 2013 +0200
@@ -1,14 +1,7 @@
 (*  Title:      Pure/Concurrent/time_limit.ML
     Author:     Makarius
 
-Execution with time limit.
-
-Notes:
-
-  * There is considerable overhead due to fork of watchdog thread.
-
-  * In rare situations asynchronous interrupts might be mistaken as
-    timeout event, and turned into exception TimeOut accidentally.
+Execution with time limit (relative timeout).
 *)
 
 signature TIME_LIMIT =
@@ -22,27 +15,22 @@
 
 exception TimeOut;
 
-val wait_time = seconds 0.0001;
-
-fun timeLimit time f x =
+fun timeLimit timeout f x =
   Multithreading.with_attributes Multithreading.no_interrupts (fn orig_atts =>
     let
-      val main = Thread.self ();
-      val timeout = Unsynchronized.ref false;
-      val watchdog = Simple_Thread.fork true (fn () =>
-        (OS.Process.sleep time; timeout := true; Simple_Thread.interrupt_unsynchronized main));
+      val self = Thread.self ();
+
+      val request =
+        Event_Timer.request (Time.+ (Time.now (), timeout))
+          (fn () => Simple_Thread.interrupt_unsynchronized self);
 
       val result =
         Exn.capture (fn () => Multithreading.with_attributes orig_atts (fn _ => f x)) ();
 
-      val _ = Simple_Thread.interrupt_unsynchronized watchdog;
-      val _ = while Thread.isActive watchdog do OS.Process.sleep wait_time;
-
-      val test = Exn.capture Multithreading.interrupted ();
+      val was_timeout = not (Event_Timer.cancel request);
     in
-      if ! timeout andalso (Exn.is_interrupt_exn result orelse Exn.is_interrupt_exn test)
+      if was_timeout andalso Exn.is_interrupt_exn result
       then raise TimeOut
-      else if Exn.is_interrupt_exn test then Exn.interrupt ()
       else Exn.release result
     end);