wenzelm [Mon, 08 Sep 2008 16:08:23 +0200] rev 28166
moved task, thread_data, group, queue to task_queue.ML;
tuned signature;
SYNCHRONIZED notify_all!
misc tuning;
wenzelm [Mon, 08 Sep 2008 16:08:18 +0200] rev 28165
Ordered queue of grouped tasks.
formerly in future.ML;
added thread data;
added group;
more robust dequeue: change into running here;
misc tuning;
wenzelm [Mon, 08 Sep 2008 16:08:13 +0200] rev 28164
added Concurrent/task_queue.ML;
wenzelm [Mon, 08 Sep 2008 00:25:34 +0200] rev 28163
await: SYNCHRONIZED wait!
wenzelm [Mon, 08 Sep 2008 00:10:41 +0200] rev 28162
tuned check_cache;
removed broken self_synchronized, which cannot be used in conjunction with condition variables;
more precise use of SYNCHRONIZED vs. wait;
tuned worker_loop;
wenzelm [Sun, 07 Sep 2008 22:20:15 +0200] rev 28161
added sync_interrupts, regular_interrupts;
max_thread_value: enforce >= 1;