src/Pure/General/timing.ML
Sat, 04 Nov 2017 12:39:25 +0100 wenzelm tuned;
Sat, 04 Nov 2017 12:25:09 +0100 wenzelm more portable print_time, notably for occasional negative (!) elapsed time of theory_timing;
Mon, 14 Aug 2017 15:30:26 +0200 wenzelm updated to scala-2.12.3;
Sat, 02 Apr 2016 23:29:05 +0200 wenzelm prefer infix operations;
Thu, 18 Dec 2014 21:10:39 +0100 wenzelm suppress irrelevant timing messages (the majority);
Mon, 31 Mar 2014 10:28:08 +0200 wenzelm support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
Tue, 09 Apr 2013 20:16:52 +0200 wenzelm just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
Wed, 03 Apr 2013 21:48:43 +0200 wenzelm additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
Wed, 20 Feb 2013 15:22:22 +0100 wenzelm more tight representation of command timing;
Tue, 19 Feb 2013 12:58:32 +0100 wenzelm support for prescient timing information within command transactions;
Wed, 09 Jan 2013 13:38:57 +0100 wenzelm standardized treatment of timing properties;
Tue, 08 Jan 2013 21:16:51 +0100 wenzelm include timing properties in log; build_history_base
Wed, 24 Aug 2011 15:30:43 +0200 wenzelm ignore irrelevant timings;
Sun, 15 May 2011 20:50:22 +0200 wenzelm only show relevant timing;
Mon, 21 Mar 2011 20:15:03 +0100 wenzelm tuned;
Sun, 20 Mar 2011 21:44:38 +0100 wenzelm pure Timing.timing, without any exception handling;
Sun, 20 Mar 2011 21:28:11 +0100 wenzelm structure Timing: covers former start_timing/end_timing and Output.timeit etc;
Sat, 06 Nov 2010 17:55:32 +0100 wenzelm somewhat more uniform timing in ML vs. Scala;
less more (0) tip