main: wait_timeout (1 second);
authorwenzelm
Wed Aug 15 22:21:13 2007 +0200 (2007-08-15)
changeset 24291fa72aab966dc
parent 24290 5607b8b752bb
child 24292 26ac9fe0e80e
main: wait_timeout (1 second);
src/Pure/ML-Systems/multithreading_polyml.ML
     1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Aug 15 20:26:57 2007 +0200
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Aug 15 22:21:13 2007 +0200
     1.3 @@ -146,6 +146,7 @@
     1.4      val wakeup = ConditionVar.conditionVar ();
     1.5      fun wakeup_all () = ConditionVar.broadcast wakeup;
     1.6      fun wait () = ConditionVar.wait (wakeup, lock);
     1.7 +    fun wait_timeout () = ConditionVar.waitUntil (wakeup, lock, Time.now () + Time.fromSeconds 1);
     1.8  
     1.9      (*queue of tasks*)
    1.10      val queue = ref tasks;
    1.11 @@ -194,7 +195,7 @@
    1.12        while not (List.null (! running)) do
    1.13        (trace_active ();
    1.14         if not (List.null (! status)) then (List.app Thread.interrupt (! running)) else ();
    1.15 -       wait ())));
    1.16 +       wait_timeout ())));
    1.17  
    1.18    in ! status end);
    1.19