src/Pure/General/time.scala
Tue, 05 Mar 2024 15:54:33 +0100 wenzelm clarified signature: incorporate guard into Logger;
Fri, 03 Nov 2023 10:30:51 +0100 wenzelm prefer Time.scale(), following Isabelle/ML;
Sun, 16 Jul 2023 11:43:32 +0200 wenzelm more operations;
Fri, 01 Apr 2022 17:06:10 +0200 wenzelm clarified formatting, for the sake of scala3;
Thu, 19 Aug 2021 12:01:57 +0200 wenzelm tuned;
Sun, 16 May 2021 13:34:27 +0200 wenzelm tuned signature --- following hints by IntelliJ IDEA;
Fri, 05 Mar 2021 16:45:16 +0100 wenzelm removed unused/pointless operation: Time.start is the load/init time of this Scala module;
Mon, 01 Mar 2021 22:22:12 +0100 wenzelm tuned --- fewer warnings;
Sat, 04 Apr 2020 18:13:05 +0200 wenzelm clarified signature;
Mon, 25 Nov 2019 12:19:14 +0100 wenzelm tuned -- avoid deprecated constructors;
Fri, 28 Apr 2017 18:24:58 +0200 wenzelm unused;
Fri, 28 Apr 2017 18:23:39 +0200 wenzelm clarified database layout;
Thu, 27 Apr 2017 23:36:16 +0200 wenzelm more encode/decode operations;
Mon, 24 Oct 2016 12:16:12 +0200 wenzelm discontinued unused / untested distinction of separate PIDE modules;
Wed, 05 Oct 2016 20:13:32 +0200 wenzelm proper calculation;
Wed, 05 Oct 2016 19:45:36 +0200 wenzelm more date and time operations from Java 8;
Sun, 14 Aug 2016 22:17:32 +0200 wenzelm clarified options and arguments;
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