src/Pure/Concurrent/task_queue.ML
2009-07-09 wenzelm 2009-07-09 renamed functor TableFun to Table, and GraphFun to Graph;
2009-06-14 wenzelm 2009-06-14 removed obsolete depend, add_job_acyclic; enqueue, finished: more careful update of cache;
2009-06-13 wenzelm 2009-06-13 simplified join_results: no longer work "towards" deps, which simplifies task queue management and maintains strict bottom up discipline (without "transfer of priority" to required futures); more efficient Task_Queue.dequeue, with internal cache (reduces wast of cycles with many idle workers); removed complicated/expensive Task_Queue.dequeue_towards;
2009-01-06 wenzelm 2009-01-06 added is_valid; added extend: support bulk jobs; tuned;
2009-01-04 wenzelm 2009-01-04 cancel: unique threads;
2009-01-03 wenzelm 2009-01-03 added eq_group; opaque signature match prevents accidental task/group equality; added cancel_all;
2008-12-16 wenzelm 2008-12-16 renamed structure TaskQueue to Task_Queue; tasks are ordered according to priority, which has been generalized from bool to int; removed unused focus; tuned dequeue: single pass due to proper priority order; tuned dequeue_towards;
2008-12-16 wenzelm 2008-12-16 tuned enqueue: plain add_edge, acyclic not required here;
2008-12-06 wenzelm 2008-12-06 added new_task;
2008-10-09 wenzelm 2008-10-09 added invalidate_group; SimpleThread.interrupt;
2008-09-27 wenzelm 2008-09-27 dequeue_towards: return bound for unfinished tasks;
2008-09-23 wenzelm 2008-09-23 IntGraph.del_node;
2008-09-19 wenzelm 2008-09-19 future tasks: support boolean priorities (true = high, false = low/irrelevant);
2008-09-11 wenzelm 2008-09-11 added is_empty;
2008-09-11 wenzelm 2008-09-11 added focus, which indicates a particular collection of high-priority tasks; tuned;
2008-09-10 wenzelm 2008-09-10 tuned;
2008-09-10 wenzelm 2008-09-10 cancel: invalidate group implicitly, via bool ref; job: moved ok flag into group; added interrupt, interrupt_external for tasks;
2008-09-09 wenzelm 2008-09-09 simplified dequeue: provide Thread.self internally; simplified cancel: interrupt running threads internally; added depend; added dequeue_towards; misc tuning;
2008-09-09 wenzelm 2008-09-09 eliminated cache, access queue efficiently via IntGraph.get_first;
2008-09-09 wenzelm 2008-09-09 human-readable printing of TaskQueue.task/group;
2008-09-09 wenzelm 2008-09-09 job: explicit 'ok' status -- false for canceled jobs; group is now non-optional; tuned signature; replaced low-level interrupts by group cancel operation; misc tuning;
2008-09-08 wenzelm 2008-09-08 proper signature constraint;
2008-09-08 wenzelm 2008-09-08 moved thread data to future.ML (again); dequeue: include group; more interrupt operations; misc tuning;
2008-09-08 wenzelm 2008-09-08 Ordered queue of grouped tasks. formerly in future.ML; added thread data; added group; more robust dequeue: change into running here; misc tuning;