main: wait_timeout (1 second);

--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Aug 15 20:26:57 2007 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Aug 15 22:21:13 2007 +0200
@@ -146,6 +146,7 @@
     val wakeup = ConditionVar.conditionVar ();
     fun wakeup_all () = ConditionVar.broadcast wakeup;
     fun wait () = ConditionVar.wait (wakeup, lock);
+    fun wait_timeout () = ConditionVar.waitUntil (wakeup, lock, Time.now () + Time.fromSeconds 1);
 
     (*queue of tasks*)
     val queue = ref tasks;
@@ -194,7 +195,7 @@
       while not (List.null (! running)) do
       (trace_active ();
        if not (List.null (! status)) then (List.app Thread.interrupt (! running)) else ();
-       wait ())));
+       wait_timeout ())));
 
   in ! status end);