src/Pure/General/time.scala
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