equal
deleted
inserted
replaced
48 (purge (); |
48 (purge (); |
49 if length (!threads) < (!max_threads) then () |
49 if length (!threads) < (!max_threads) then () |
50 else (tracing ("Waiting for a free thread..."); |
50 else (tracing ("Waiting for a free thread..."); |
51 ConditionVar.wait (thread_wait, thread_wait_mutex)); |
51 ConditionVar.wait (thread_wait, thread_wait_mutex)); |
52 add_thread |
52 add_thread |
53 (Thread.fork |
53 (Thread.fork (* FIXME avoid low-level Poly/ML thread primitives *) |
54 (fn () => exception_trace threadf, |
54 (fn () => exception_trace threadf, |
55 [Thread.EnableBroadcastInterrupt true, |
55 [Thread.EnableBroadcastInterrupt true, |
56 Thread.InterruptState |
56 Thread.InterruptState |
57 Thread.InterruptAsynchOnce]))) |
57 Thread.InterruptAsynchOnce]))) |
58 end; |
58 end; |