src/Pure/Concurrent/task_queue.ML
Thu, 09 Sep 2010 17:20:27 +0200 wenzelm more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
Tue, 20 Jul 2010 17:35:42 +0200 wenzelm back to more strict dependencies, even for canceled groups (reverting parts of 02936e77a07c);
Mon, 31 May 2010 21:06:57 +0200 wenzelm modernized some structure names, keeping a few legacy aliases;
Fri, 19 Feb 2010 22:25:26 +0100 wenzelm eliminated opaque signature matching -- tends to cause problems with toplevel pp for abstract types;
Sat, 06 Feb 2010 16:32:34 +0100 wenzelm removed unused "boundary" of Table/Graph.get_first;
Wed, 06 Jan 2010 18:14:16 +0100 wenzelm 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);
Wed, 06 Jan 2010 15:07:56 +0100 wenzelm tasks of canceled groups are considered "ready" -- enables to purge the queue from tasks depending on unfinished promises (also improves general reactivity);
Tue, 05 Jan 2010 23:38:10 +0100 wenzelm added Future.promise/fulfill -- promised futures that are fulfilled by external means;
less more (0) -30 -10 -8 tip