src/Pure/General/timing.scala
2014-04-24 wenzelm 2014-04-24 tuned signature, in accordance to ML version;
2014-02-20 wenzelm 2014-02-20 tuned imports;
2013-03-30 wenzelm 2013-03-30 more operations on Time, Timing;
2012-04-21 wenzelm 2012-04-21 some builtin session timing;
2012-03-03 wenzelm 2012-03-03 relevant timing as in ML; more PIDE modules;
2011-11-29 wenzelm 2011-11-29 clarified Time vs. Timing;
2011-11-29 wenzelm 2011-11-29 separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
2011-11-28 wenzelm 2011-11-28 explicit indication of modules for independent Scala library;
2011-11-28 wenzelm 2011-11-28 tuned signature (according to ML version);
2011-10-22 wenzelm 2011-10-22 class Time as abstract datatype;
2011-09-04 wenzelm 2011-09-04 property "tooltip-dismiss-delay" is edited in ms, not seconds; explicit tooltip_dismiss_delay boundaries for further robustness;
2010-12-02 wenzelm 2010-12-02 builtin time bounds (again);
2010-12-01 wenzelm 2010-12-01 more abstract/uniform handling of time, preferring seconds as Double;
2010-11-06 wenzelm 2010-11-06 somewhat more uniform timing in ML vs. Scala;