more informative JSON results;

clarified signature;

unused;

clarified database layout;

more encode/decode operations;

more permissive timing data;

more operations;

clarified messages, notably on Windows where CPU time of poly.exe is not measured;

print timing like lib/scripts/timestop.bash;

tuned;

more systematic Isabelle output, like in classic Isabelle/ML (without markup);

tuned signature, in accordance to ML version;

tuned imports;

more operations on Time, Timing;

some builtin session timing;

relevant timing as in ML;
more PIDE modules;

clarified Time vs. Timing;

--HG--
rename : src/Pure/General/timing.scala => src/Pure/General/time.scala

separate compilation of PIDE vs. Pure sources, which enables independent Scala library;

explicit indication of modules for independent Scala library;

tuned signature (according to ML version);

class Time as abstract datatype;

property "tooltip-dismiss-delay" is edited in ms, not seconds;
explicit tooltip_dismiss_delay boundaries for further robustness;

builtin time bounds (again);

more abstract/uniform handling of time, preferring seconds as Double;

somewhat more uniform timing in ML vs. Scala;

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