#
2e95e2f5 |
|
24-Nov-2019 |
wenzelm <none@none> |
tuned -- avoid deprecated constructors;
|
#
42c130e1 |
|
28-Apr-2017 |
wenzelm <none@none> |
unused;
|
#
e0f0b463 |
|
28-Apr-2017 |
wenzelm <none@none> |
clarified database layout;
|
#
63232de5 |
|
27-Apr-2017 |
wenzelm <none@none> |
more encode/decode operations;
|
#
3ee6c0a8 |
|
23-Oct-2016 |
wenzelm <none@none> |
discontinued unused / untested distinction of separate PIDE modules;
|
#
600f6598 |
|
05-Oct-2016 |
wenzelm <none@none> |
proper calculation;
|
#
fb9a68e8 |
|
05-Oct-2016 |
wenzelm <none@none> |
more date and time operations from Java 8;
|
#
a52ae09f |
|
14-Aug-2016 |
wenzelm <none@none> |
clarified options and arguments; tuned;
|
#
f6649a01 |
|
13-Aug-2016 |
wenzelm <none@none> |
gnuplot presentation similar to former isatest-statistics;
|
#
2263201c |
|
12-Aug-2016 |
wenzelm <none@none> |
statistics from session build output;
|
#
4b8fdecc |
|
09-Mar-2016 |
wenzelm <none@none> |
print timing like lib/scripts/timestop.bash;
|
#
6f977afc |
|
08-Nov-2015 |
wenzelm <none@none> |
added option timeout_scale;
|
#
25885a56 |
|
31-Oct-2015 |
wenzelm <none@none> |
global start time as reference point;
|
#
268b5fb9 |
|
12-Aug-2014 |
wenzelm <none@none> |
tuned;
|
#
fba3db4e |
|
24-Apr-2014 |
wenzelm <none@none> |
tuned signature, in accordance to ML version;
|
#
913fb30e |
|
01-Apr-2014 |
wenzelm <none@none> |
simplified using "value class";
|
#
5ec10b0f |
|
29-Aug-2013 |
wenzelm <none@none> |
option to insert unique completion immediately into buffer;
|
#
482e71a7 |
|
30-Mar-2013 |
wenzelm <none@none> |
more operations on Time, Timing;
|
#
46957350 |
|
26-Mar-2013 |
wenzelm <none@none> |
dockable window for timing information;
|
#
97f383a0 |
|
30-Nov-2012 |
wenzelm <none@none> |
tuned import;
|
#
108b84f3 |
|
24-May-2012 |
wenzelm <none@none> |
less warning in scala-2.10.0-M3;
|
#
c613e20a |
|
03-Mar-2012 |
wenzelm <none@none> |
relevant timing as in ML; more PIDE modules;
|
#
78b39fdb |
|
27-Feb-2012 |
wenzelm <none@none> |
prefer final ADTs -- prevent ooddities;
|
#
cc9cbc32 |
|
29-Nov-2011 |
wenzelm <none@none> |
clarified Time vs. Timing; --HG-- rename : src/Pure/General/timing.scala => src/Pure/General/time.scala
|