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