| Sun, 04 Jan 2009 00:00:03 +0100 |
wenzelm |
cancel: unique threads;
|
file |
diff |
annotate
|
| Sat, 03 Jan 2009 21:44:24 +0100 |
wenzelm |
added eq_group;
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 16:25:19 +0100 |
wenzelm |
renamed structure TaskQueue to Task_Queue;
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 00:19:47 +0100 |
wenzelm |
tuned enqueue: plain add_edge, acyclic not required here;
|
file |
diff |
annotate
|
| Sat, 06 Dec 2008 00:02:11 +0100 |
wenzelm |
added new_task;
|
file |
diff |
annotate
|
| Thu, 09 Oct 2008 20:53:20 +0200 |
wenzelm |
added invalidate_group;
|
file |
diff |
annotate
|
| Sat, 27 Sep 2008 18:18:08 +0200 |
wenzelm |
dequeue_towards: return bound for unfinished tasks;
|
file |
diff |
annotate
|
| Tue, 23 Sep 2008 15:48:54 +0200 |
wenzelm |
IntGraph.del_node;
|
file |
diff |
annotate
|
| Fri, 19 Sep 2008 21:22:31 +0200 |
wenzelm |
future tasks: support boolean priorities (true = high, false = low/irrelevant);
|
file |
diff |
annotate
|
| Thu, 11 Sep 2008 21:04:07 +0200 |
wenzelm |
added is_empty;
|
file |
diff |
annotate
|
| Thu, 11 Sep 2008 18:07:58 +0200 |
wenzelm |
added focus, which indicates a particular collection of high-priority tasks;
|
file |
diff |
annotate
|
| Wed, 10 Sep 2008 23:19:36 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 10 Sep 2008 19:44:28 +0200 |
wenzelm |
cancel: invalidate group implicitly, via bool ref;
|
file |
diff |
annotate
|
| Tue, 09 Sep 2008 23:30:00 +0200 |
wenzelm |
simplified dequeue: provide Thread.self internally;
|
file |
diff |
annotate
|
| Tue, 09 Sep 2008 20:22:40 +0200 |
wenzelm |
eliminated cache, access queue efficiently via IntGraph.get_first;
|
file |
diff |
annotate
|
| Tue, 09 Sep 2008 16:59:48 +0200 |
wenzelm |
human-readable printing of TaskQueue.task/group;
|
file |
diff |
annotate
|
| Tue, 09 Sep 2008 16:29:32 +0200 |
wenzelm |
job: explicit 'ok' status -- false for canceled jobs;
|
file |
diff |
annotate
|
| Mon, 08 Sep 2008 21:08:30 +0200 |
wenzelm |
proper signature constraint;
|
file |
diff |
annotate
|
| Mon, 08 Sep 2008 20:33:27 +0200 |
wenzelm |
moved thread data to future.ML (again);
|
file |
diff |
annotate
|
| Mon, 08 Sep 2008 16:08:18 +0200 |
wenzelm |
Ordered queue of grouped tasks.
|
file |
diff |
annotate
|