| Mon, 31 Jan 2011 22:57:01 +0100 |
wenzelm |
support named tasks, for improved tracing;
|
file |
diff |
annotate
|
| Mon, 31 Jan 2011 21:54:49 +0100 |
wenzelm |
more direct Future.bulk, which potentially reduces overhead for Par_List;
|
file |
diff |
annotate
|
| Thu, 25 Nov 2010 16:12:23 +0100 |
wenzelm |
clarified Par_List.managed_results, with explicit propagation of outermost physical interrupt to forked futures (e.g. to make timeout apply here as expected and prevent zombies);
|
file |
diff |
annotate
|
| Wed, 21 Jul 2010 13:25:14 +0200 |
wenzelm |
clarified/exported Future.worker_subgroup, which is already the default for Future.fork;
|
file |
diff |
annotate
|
| Sat, 27 Feb 2010 13:31:55 +0100 |
wenzelm |
degrade gracefully in CRITICAL section;
|
file |
diff |
annotate
|
| Sun, 20 Sep 2009 17:23:23 +0200 |
wenzelm |
actually observe Multithreading.enabled (cf. d302f1c9e356);
|
file |
diff |
annotate
|
| Tue, 28 Jul 2009 16:30:23 +0200 |
wenzelm |
eliminated separate Future.enabled -- let Future.join fail explicitly in critical section, instead of entering sequential mode silently;
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 20:37:31 +0200 |
wenzelm |
map: subgroup of worker_group;
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 10:24:57 +0200 |
wenzelm |
prefer simultaneous join -- for improved scheduling;
|
file |
diff |
annotate
|
| Tue, 06 Jan 2009 14:43:35 +0100 |
wenzelm |
renamed structure ParList to Par_List;
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 16:25:19 +0100 |
wenzelm |
renamed structure TaskQueue to Task_Queue;
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 23:46:20 +0100 |
wenzelm |
refined Future.fork interfaces, no longer export Future.future;
|
file |
diff |
annotate
|
| Tue, 21 Oct 2008 16:52:59 +0200 |
wenzelm |
Future.join_result;
|
file |
diff |
annotate
|
| Tue, 21 Oct 2008 15:01:18 +0200 |
wenzelm |
added Future.enabled check;
|
file |
diff |
annotate
|
| Thu, 09 Oct 2008 20:53:16 +0200 |
wenzelm |
subject to Multithreading.enabled;
|
file |
diff |
annotate
|
| Wed, 01 Oct 2008 12:00:02 +0200 |
wenzelm |
more robust treatment of Interrupt (cf. exn.ML);
|
file |
diff |
annotate
|
| Sat, 27 Sep 2008 18:18:07 +0200 |
wenzelm |
moved release_results to future.ML;
|
file |
diff |
annotate
|
| Thu, 25 Sep 2008 14:37:32 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Thu, 25 Sep 2008 14:35:03 +0200 |
wenzelm |
added release_results;
|
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 13:24:14 +0200 |
wenzelm |
Parallel list combinators.
|
file |
diff |
annotate
|