# HG changeset patch
# User wenzelm
# Date 1187209273 -7200
# Node ID fa72aab966dca6c3c022d57a5d0e7a1af34f4f50
# Parent  5607b8b752bba3442fd7babdebc62a46a24c87ae
main: wait_timeout (1 second);

diff -r 5607b8b752bb -r fa72aab966dc src/Pure/ML-Systems/multithreading_polyml.ML
--- 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);