Tue, 14 May 2013 20:46:09 +0200 | wenzelm | more uniform Markup.print_real; | file | diff | annotate |
Fri, 18 Jan 2013 17:51:50 +0100 | wenzelm | more systematic task statistics; | file | diff | annotate |
Wed, 11 Apr 2012 13:49:09 +0200 | wenzelm | more robust Future.fulfill wrt. duplicate assignment and interrupt; | file | diff | annotate |
Mon, 09 Apr 2012 17:22:23 +0200 | wenzelm | simplified Future.cancel/cancel_group (again) -- running threads only; | file | diff | annotate |
Sat, 26 Nov 2011 13:10:12 +0100 | wenzelm | tuned; | file | diff | annotate |
Sun, 06 Nov 2011 13:25:41 +0100 | wenzelm | optional timing, to avoid redundant allocation of mutable cells; | file | diff | annotate |
Thu, 13 Oct 2011 22:50:35 +0200 | wenzelm | static dummy_task (again) to avoid a few extra allocations; | file | diff | annotate |