src/Pure/Concurrent/par_list.ML
2009-09-20 wenzelm 2009-09-20 actually observe Multithreading.enabled (cf. d302f1c9e356);
2009-07-28 wenzelm 2009-07-28 eliminated separate Future.enabled -- let Future.join fail explicitly in critical section, instead of entering sequential mode silently;
2009-07-21 wenzelm 2009-07-21 map: subgroup of worker_group;
2009-07-21 wenzelm 2009-07-21 prefer simultaneous join -- for improved scheduling;
2009-01-06 wenzelm 2009-01-06 renamed structure ParList to Par_List;
2008-12-16 wenzelm 2008-12-16 renamed structure TaskQueue to Task_Queue;
2008-12-04 wenzelm 2008-12-04 refined Future.fork interfaces, no longer export Future.future;
2008-10-21 wenzelm 2008-10-21 Future.join_result;
2008-10-21 wenzelm 2008-10-21 added Future.enabled check;
2008-10-09 wenzelm 2008-10-09 subject to Multithreading.enabled; raw_map: join sequentially, less overhead;
2008-10-01 wenzelm 2008-10-01 more robust treatment of Interrupt (cf. exn.ML);
2008-09-27 wenzelm 2008-09-27 moved release_results to future.ML; get_some: simplified via Future.release_results;
2008-09-25 wenzelm 2008-09-25 tuned comments;
2008-09-25 wenzelm 2008-09-25 added release_results; tuned comments;
2008-09-19 wenzelm 2008-09-19 future tasks: support boolean priorities (true = high, false = low/irrelevant);
2008-09-11 wenzelm 2008-09-11 Parallel list combinators.