| Thu, 28 Nov 2013 12:54:39 +0100 | wenzelm | more official task context via Task_Queue.enroll, which is required to participate in group cancellation (e.g. to terminate command exec); | file | diff | annotate |
| Sun, 25 Aug 2013 17:04:22 +0200 | wenzelm | simplified Goal.forked_proofs: status is determined via group instead of dummy future (see also Pure/PIDE/execution.ML); | file | diff | annotate |
| Mon, 08 Jul 2013 12:00:45 +0200 | wenzelm | allow worker guest threads, which participate actively in future joins, but are outside thread accounting; | file | diff | annotate |