src/Pure/Concurrent/par_list.ML
Wed, 17 Aug 2011 22:14:22 +0200 wenzelm more systematic handling of parallel exceptions;
Wed, 10 Aug 2011 16:05:14 +0200 wenzelm future_job: explicit indication of interrupts;
Sat, 05 Feb 2011 20:38:32 +0100 wenzelm more tracing information via Par_List.map_name;
Mon, 31 Jan 2011 23:10:16 +0100 wenzelm tuned trivial cases;
Mon, 31 Jan 2011 23:02:53 +0100 wenzelm tuned signature;
Mon, 31 Jan 2011 22:57:01 +0100 wenzelm support named tasks, for improved tracing;
Mon, 31 Jan 2011 21:54:49 +0100 wenzelm more direct Future.bulk, which potentially reduces overhead for Par_List;
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);
Wed, 21 Jul 2010 13:25:14 +0200 wenzelm clarified/exported Future.worker_subgroup, which is already the default for Future.fork;
Sat, 27 Feb 2010 13:31:55 +0100 wenzelm degrade gracefully in CRITICAL section;
Sun, 20 Sep 2009 17:23:23 +0200 wenzelm actually observe Multithreading.enabled (cf. d302f1c9e356);
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;
Tue, 21 Jul 2009 20:37:31 +0200 wenzelm map: subgroup of worker_group;
Tue, 21 Jul 2009 10:24:57 +0200 wenzelm prefer simultaneous join -- for improved scheduling;
Tue, 06 Jan 2009 14:43:35 +0100 wenzelm renamed structure ParList to Par_List;
Tue, 16 Dec 2008 16:25:19 +0100 wenzelm renamed structure TaskQueue to Task_Queue;
Thu, 04 Dec 2008 23:46:20 +0100 wenzelm refined Future.fork interfaces, no longer export Future.future;
Tue, 21 Oct 2008 16:52:59 +0200 wenzelm Future.join_result;
Tue, 21 Oct 2008 15:01:18 +0200 wenzelm added Future.enabled check;
Thu, 09 Oct 2008 20:53:16 +0200 wenzelm subject to Multithreading.enabled;
Wed, 01 Oct 2008 12:00:02 +0200 wenzelm more robust treatment of Interrupt (cf. exn.ML);
Sat, 27 Sep 2008 18:18:07 +0200 wenzelm moved release_results to future.ML;
Thu, 25 Sep 2008 14:37:32 +0200 wenzelm tuned comments;
Thu, 25 Sep 2008 14:35:03 +0200 wenzelm added release_results;
Fri, 19 Sep 2008 21:22:31 +0200 wenzelm future tasks: support boolean priorities (true = high, false = low/irrelevant);
Thu, 11 Sep 2008 13:24:14 +0200 wenzelm Parallel list combinators.
less more (0) tip