src/Pure/Concurrent/future.ML
2008-10-02 ago added simple heartbeat thread;
2008-10-02 ago more tuning of tracing messages;
2008-10-02 ago tuned SYNCHRONIZED: outermost Exn.release;
2008-10-01 ago removed release_results (cf. Exn.release_all, Exn.release_first);
2008-09-30 ago renamed Future.fork_irrelevant to Future.fork_background;
2008-09-29 ago added str_of;
2008-09-28 ago proper setmp_thread_data for nested execute (cf. join_loop);
2008-09-28 ago thread_data: include thread name, export access;
2008-09-27 ago added release_results (formerly in par_list.ML);
2008-09-27 ago more tracing;
2008-09-23 ago join_results: special case for empty list, works without multithreading;
2008-09-22 ago added is_finished;
2008-09-19 ago future tasks: support boolean priorities (true = high, false = low/irrelevant);
2008-09-17 ago shutdown only if Multithreading.available;
2008-09-16 ago SimpleThread.fork;
2008-09-11 ago cancel, shutdown: notify_all;
2008-09-11 ago eliminated requests, use global state variables uniformly;
2008-09-11 ago shutdown: global join-and-shutdown operation;
2008-09-11 ago added focus, which indicates a particular collection of high-priority tasks;
2008-09-11 ago some general notes on future values;
2008-09-10 ago added interrupt_task (external id);
2008-09-10 ago replaced join_all by join_results, which returns Exn.results;
2008-09-10 ago workers: explicit activity flag;
2008-09-10 ago future: allow explicit group;
2008-09-09 ago cancel: check_scheduler;
2008-09-09 ago inherit group from running thread, or create a new one -- make it harder to re-use canceled groups;
2008-09-08 ago tuned Mailbox.send;
2008-09-08 ago more interrupt operations;
2008-09-08 ago moved task, thread_data, group, queue to task_queue.ML;
2008-09-08 ago await: SYNCHRONIZED wait!
2008-09-08 ago tuned check_cache;
2008-09-07 ago Functional threads as future values.