src/Pure/General/time.scala
Sat, 13 Aug 2016 23:45:29 +0200 wenzelm gnuplot presentation similar to former isatest-statistics;
Sat, 13 Aug 2016 12:06:11 +0200 wenzelm statistics from session build output;
Wed, 09 Mar 2016 16:42:30 +0100 wenzelm print timing like lib/scripts/timestop.bash;
Sun, 08 Nov 2015 14:41:07 +0100 wenzelm added option timeout_scale;
Sat, 31 Oct 2015 14:16:29 +0100 wenzelm global start time as reference point;
Tue, 12 Aug 2014 15:46:20 +0200 wenzelm tuned;
Thu, 24 Apr 2014 11:01:14 +0200 wenzelm tuned signature, in accordance to ML version;
Tue, 01 Apr 2014 16:16:25 +0200 wenzelm simplified using "value class";
Thu, 29 Aug 2013 21:17:46 +0200 wenzelm option to insert unique completion immediately into buffer;
Sat, 30 Mar 2013 16:15:26 +0100 wenzelm more operations on Time, Timing;
Tue, 26 Mar 2013 11:26:13 +0100 wenzelm dockable window for timing information;
Fri, 30 Nov 2012 21:28:35 +0100 wenzelm tuned import;
Thu, 24 May 2012 22:07:00 +0200 wenzelm less warning in scala-2.10.0-M3;
Sat, 03 Mar 2012 11:09:17 +0100 wenzelm relevant timing as in ML;
Mon, 27 Feb 2012 17:13:25 +0100 wenzelm prefer final ADTs -- prevent ooddities;
Tue, 29 Nov 2011 21:50:00 +0100 wenzelm clarified Time vs. Timing;
less more (0) tip