| 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
|