src/Pure/Concurrent/future.ML
2008-10-01 wenzelm 2008-10-01 removed release_results (cf. Exn.release_all, Exn.release_first);
2008-09-30 wenzelm 2008-09-30 renamed Future.fork_irrelevant to Future.fork_background; tuned;
2008-09-29 wenzelm 2008-09-29 added str_of;
2008-09-28 wenzelm 2008-09-28 proper setmp_thread_data for nested execute (cf. join_loop);
2008-09-28 wenzelm 2008-09-28 thread_data: include thread name, export access; more tracing;
2008-09-27 wenzelm 2008-09-27 added release_results (formerly in par_list.ML); more informative trace_active; join_results: avoid deadlock via nested SYNCHRONOIZED, more robust active join, less rechecking of tasks;
2008-09-27 wenzelm 2008-09-27 more tracing;
2008-09-23 wenzelm 2008-09-23 join_results: special case for empty list, works without multithreading;
2008-09-22 wenzelm 2008-09-22 added is_finished;
2008-09-19 wenzelm 2008-09-19 future tasks: support boolean priorities (true = high, false = low/irrelevant);
2008-09-17 wenzelm 2008-09-17 shutdown only if Multithreading.available;
2008-09-16 wenzelm 2008-09-16 SimpleThread.fork;
2008-09-11 wenzelm 2008-09-11 cancel, shutdown: notify_all;
2008-09-11 wenzelm 2008-09-11 eliminated requests, use global state variables uniformly; more robust shutdown;
2008-09-11 wenzelm 2008-09-11 shutdown: global join-and-shutdown operation; reduced trace_active; scheduler_fork: always notify; tracing for thread exit; unique ids for workers;
2008-09-11 wenzelm 2008-09-11 added focus, which indicates a particular collection of high-priority tasks; tuned;
2008-09-11 wenzelm 2008-09-11 some general notes on future values;
2008-09-10 wenzelm 2008-09-10 added interrupt_task (external id); tuned signature;
2008-09-10 wenzelm 2008-09-10 replaced join_all by join_results, which returns Exn.results; join: disallow Multithreading.self_critical, which is prone to deadlocks due to context change via fork;
2008-09-10 wenzelm 2008-09-10 workers: explicit activity flag; SYNCHRONIZED: optional tracing;
2008-09-10 wenzelm 2008-09-10 future: allow explicit group; cancel: invalidate group identifier for all future members; tuned comments; tuned;
2008-09-09 wenzelm 2008-09-09 cancel: check_scheduler; adapted to simplified TaskQueue.cancel; improved join/join_all: actively work towards results, i.e. do not yield unnecessarily; misc tuning;
2008-09-09 wenzelm 2008-09-09 inherit group from running thread, or create a new one -- make it harder to re-use canceled groups; group is now non-optional; tuned signature; replaced low-level interrupts by group cancel operation; misc tuning;
2008-09-08 wenzelm 2008-09-08 tuned Mailbox.send;
2008-09-08 wenzelm 2008-09-08 more interrupt operations; maintain thread data (formerly in task_queue.ML); wait: added tracing; added requests mailbox; handle excessive workers fork: inherit group; added rudimentary shutdown; misc tuning;
2008-09-08 wenzelm 2008-09-08 moved task, thread_data, group, queue to task_queue.ML; tuned signature; SYNCHRONIZED notify_all! misc tuning;
2008-09-08 wenzelm 2008-09-08 await: SYNCHRONIZED wait!
2008-09-08 wenzelm 2008-09-08 tuned check_cache; removed broken self_synchronized, which cannot be used in conjunction with condition variables; more precise use of SYNCHRONIZED vs. wait; tuned worker_loop;
2008-09-07 wenzelm 2008-09-07 Functional threads as future values.