src/Pure/General/timing.scala
Sat, 22 Oct 2011 23:29:11 +0200 wenzelm class Time as abstract datatype;
Sun, 04 Sep 2011 15:49:59 +0200 wenzelm property "tooltip-dismiss-delay" is edited in ms, not seconds;
Thu, 02 Dec 2010 10:46:03 +0100 wenzelm builtin time bounds (again);
Wed, 01 Dec 2010 20:34:40 +0100 wenzelm more abstract/uniform handling of time, preferring seconds as Double;
Sat, 06 Nov 2010 17:55:32 +0100 wenzelm somewhat more uniform timing in ML vs. Scala;
less more (0) tip