src/Pure/General/timing.ML
12 months ago wenzelm 2017-11-04 tuned;
12 months ago wenzelm 2017-11-04 more portable print_time, notably for occasional negative (!) elapsed time of theory_timing;
15 months ago wenzelm 2017-08-14 updated to scala-2.12.3;
2016-04-02 wenzelm 2016-04-02 prefer infix operations;
2014-12-18 wenzelm 2014-12-18 suppress irrelevant timing messages (the majority);
2014-03-31 wenzelm 2014-03-31 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;
2013-04-09 wenzelm 2013-04-09 just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
2013-04-03 wenzelm 2013-04-03 additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
2013-02-20 wenzelm 2013-02-20 more tight representation of command timing; tuned signatures; tuned;
2013-02-19 wenzelm 2013-02-19 support for prescient timing information within command transactions;
2013-01-09 wenzelm 2013-01-09 standardized treatment of timing properties;
2013-01-08 wenzelm 2013-01-08 include timing properties in log; general Properties.parse operations; tuned signature;
2011-08-24 wenzelm 2011-08-24 ignore irrelevant timings;
2011-05-15 wenzelm 2011-05-15 only show relevant timing;
2011-03-21 wenzelm 2011-03-21 tuned;
2011-03-20 wenzelm 2011-03-20 pure Timing.timing, without any exception handling; clarified cond_timeit: propagate interrupt without side-effect;
2011-03-20 wenzelm 2011-03-20 structure Timing: covers former start_timing/end_timing and Output.timeit etc; explicit Timing.message function; eliminated Output.timing flag, cf. Toplevel.timing; tuned;
2010-11-06 wenzelm 2010-11-06 somewhat more uniform timing in ML vs. Scala;