src/Pure/ML/ml_statistics.scala
2017-05-18 wenzelm 2017-05-18 uniform heap_scale; tuned;
2017-05-18 wenzelm 2017-05-18 simplified signature;
2017-05-17 wenzelm 2017-05-17 more systematic maximum and average; tuned;
2017-05-17 wenzelm 2017-05-17 store processed content instead of somewhat bulky properties;
2017-05-17 wenzelm 2017-05-17 include full ML statistics: max heap size;
2017-05-17 wenzelm 2017-05-17 tuned signature;
2017-04-13 wenzelm 2017-04-13 clarified directories;
2013-01-18 wenzelm 2013-01-18 added "tasks_proof" statistics, via slighly odd global reference Future.forked_proofs (NB: Future.report_status is intertwined with scheduler thread);
2013-01-12 wenzelm 2013-01-12 proper window title;
2013-01-12 wenzelm 2013-01-12 add icon for toplevel windows;
2013-01-08 wenzelm 2013-01-08 include timing properties in log; general Properties.parse operations; tuned signature;
2013-01-03 wenzelm 2013-01-03 improved Monitor_Dockable, based on ML_Statistics operations; tuned signature;
2013-01-02 wenzelm 2013-01-02 added standard_frames convenience;
2013-01-02 wenzelm 2013-01-02 some grouping of standard fields; tuned signature;
2013-01-02 wenzelm 2013-01-02 some support for chart drawing;
2013-01-02 wenzelm 2013-01-02 some support for ML statistics content interpretation;
2013-01-02 wenzelm 2013-01-02 ML runtime statistics: read properties from build log;