2016-04-02 ago prefer infix operations;
2016-04-02 ago careful export of type-dependent functions, without losing their special status;
2016-03-18 ago clarified modules;
2015-06-29 ago improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
2015-01-09 ago clarified active_job: take dependencies into account (e.g. future based on promise);
2015-01-09 ago tuned;
2013-11-28 ago more official task context via Task_Queue.enroll, which is required to participate in group cancellation (e.g. to terminate command exec);
2013-08-25 ago simplified Goal.forked_proofs: status is determined via group instead of dummy future (see also Pure/PIDE/execution.ML);
2013-07-08 ago allow worker guest threads, which participate actively in future joins, but are outside thread accounting;
2013-07-05 ago more uniform Counter in ML and Scala;
2013-05-14 ago more uniform Markup.print_real;
2013-01-18 ago more systematic task statistics;
2012-04-11 ago more robust Future.fulfill wrt. duplicate assignment and interrupt;
2012-04-09 ago simplified Future.cancel/cancel_group (again) -- running threads only;
2011-11-26 ago tuned;
2011-11-06 ago optional timing, to avoid redundant allocation of mutable cells;
2011-10-13 ago static dummy_task (again) to avoid a few extra allocations;
2011-08-21 ago purely functional task_queue.ML -- moved actual interrupt_unsynchronized to future.ML;
2011-08-21 ago refined Task_Queue.cancel: passive tasks are considered running due to pending abort operation;
2011-08-20 ago refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
2011-08-19 ago refined Future.cancel: explicit future allows to join actual cancellation;
2011-08-17 ago more systematic handling of parallel exceptions;
2011-08-10 ago more explicit Simple_Thread.interrupt_unsynchronized, to emphasize its meaning;
2011-07-23 ago more detailed tracing;
2011-07-13 ago Table.lookup_key and Graph.get_entry allow to retrieve the original key, which is not necessarily identical to the given one;
2011-02-04 ago more scalable collections of tasks, notably for totality of known group members;
2011-02-04 ago tuned signature;
2011-02-04 ago Task_Queue.update_timing: more precise treatment of interruptibility;
2011-02-02 ago eliminated slightly odd abstract type Task_Queue.deps;
2011-02-02 ago refined Task_Queue.dequeue_deps (more incremental);
2011-02-02 ago maintain within Task_Queue.task;
2011-02-02 ago tuned comment;
2011-02-02 ago Future.join_results: discontinued post-hoc recording of dynamic dependencies;
2011-02-01 ago more informative task timing: some dependency tracking;
2011-02-01 ago refined task timing: joining vs. waiting;
2011-01-31 ago name "passive" tasks (practically lazy values);
2011-01-31 ago support named tasks, for improved tracing;
2011-01-31 ago added basic task timing;
2010-11-09 ago private counter, to keep externalized ids a bit smaller;
2010-09-10 ago Future.promise: more robust treatment of concurrent abort vs. fulfill (amending 047c96f41455);
2010-09-09 ago more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
2010-07-20 ago back to more strict dependencies, even for canceled groups (reverting parts of 02936e77a07c);
2010-05-31 ago modernized some structure names, keeping a few legacy aliases;
2010-02-19 ago eliminated opaque signature matching -- tends to cause problems with toplevel pp for abstract types;
2010-02-06 ago removed unused "boundary" of Table/Graph.get_first;
2010-01-06 ago eliminated cache, which complicates the code without making a real difference (NB: deque_towards often disrupts caching, and daisy-chaining of workers already reduces queue overhead);
2010-01-06 ago tasks of canceled groups are considered "ready" -- enables to purge the queue from tasks depending on unfinished promises (also improves general reactivity);
2010-01-05 ago added Future.promise/fulfill -- promised futures that are fulfilled by external means;
2009-10-01 ago added Task_Queue.depend (again) -- light-weight version for transitive graph;
2009-09-30 ago eliminated redundant bindings;
2009-07-28 ago group status: Synchronized.var;
2009-07-28 ago tuned;
2009-07-28 ago Task_Queue.dequeue: explicit thread;
2009-07-27 ago dequeue_towards: always return active tasks;
2009-07-27 ago removed unused low-level interrupts;
2009-07-27 ago tuned signature;
2009-07-27 ago enqueue/finish: return minimal/maximal state of this task;
2009-07-25 ago dequeue_towards: need to try imm_preds as well;
2009-07-25 ago enqueue: maintain transitive closure, which simplifies dequeue_towards;
2009-07-21 ago support for nested groups -- cancellation is propagated to peers and subgroups;