src/Pure/Tools/build.ML
Tue, 19 Feb 2013 10:55:11 +0100 wenzelm emit command_timing properties into build log;
Thu, 24 Jan 2013 17:18:13 +0100 wenzelm more efficient inlined properties, especially relevant for voluminous tasks trace;
Fri, 18 Jan 2013 23:33:17 +0100 wenzelm use inlined session name as title for charts;
Fri, 18 Jan 2013 17:51:50 +0100 wenzelm more systematic task statistics;
Sat, 12 Jan 2013 15:00:48 +0100 wenzelm immediate theory progress for build_dialog;
Tue, 08 Jan 2013 21:16:51 +0100 wenzelm include timing properties in log; build_history_base
Thu, 03 Jan 2013 20:42:18 +0100 wenzelm maintain session index on Scala side, for more determistic results;
Thu, 03 Jan 2013 14:03:44 +0100 wenzelm always enable Future.ML_statistics where this makes sense -- runtime overhead should be negligible;
Wed, 02 Jan 2013 17:58:53 +0100 wenzelm moved files;
less more (0) tip