clarified signature;

tuned;

more portable print_time, notably for occasional negative (!) elapsed time of theory_timing;

updated to scala-2.12.3;

prefer infix operations;

suppress irrelevant timing messages (the majority);

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;

just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;

additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;

more tight representation of command timing;
tuned signatures;
tuned;

support for prescient timing information within command transactions;

standardized treatment of timing properties;

include timing properties in log;
general Properties.parse operations;
tuned signature;

ignore irrelevant timings;

only show relevant timing;

tuned;

pure Timing.timing, without any exception handling;
clarified cond_timeit: propagate interrupt without side-effect;

structure Timing: covers former start_timing/end_timing and Output.timeit etc;
explicit Timing.message function;
eliminated Output.timing flag, cf. Toplevel.timing;
tuned;

somewhat more uniform timing in ML vs. Scala;

--HG--
rename : src/Pure/ML-Systems/timing.ML => src/Pure/General/timing.ML