src/Pure/ML/ml_statistics.scala
Wed, 20 Feb 2019 12:10:40 +0100 wenzelm updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
Wed, 09 May 2018 19:53:37 +0200 wenzelm record total number of tasks;
Sat, 03 Mar 2018 21:38:27 +0100 wenzelm more compact ML_Statistics, to make build_status work with less than 2GB heap;
Thu, 18 May 2017 14:38:09 +0200 wenzelm uniform heap_scale;
Thu, 18 May 2017 13:51:25 +0200 wenzelm simplified signature;
Wed, 17 May 2017 22:27:33 +0200 wenzelm more systematic maximum and average;
Wed, 17 May 2017 20:52:24 +0200 wenzelm store processed content instead of somewhat bulky properties;
Wed, 17 May 2017 14:58:48 +0200 wenzelm include full ML statistics: max heap size;
Wed, 17 May 2017 13:47:19 +0200 wenzelm tuned signature;
Thu, 13 Apr 2017 12:27:57 +0200 wenzelm clarified directories;
Fri, 18 Jan 2013 16:20:09 +0100 wenzelm added "tasks_proof" statistics, via slighly odd global reference Future.forked_proofs (NB: Future.report_status is intertwined with scheduler thread);
Sat, 12 Jan 2013 22:14:29 +0100 wenzelm proper window title;
Sat, 12 Jan 2013 22:08:38 +0100 wenzelm add icon for toplevel windows;
Tue, 08 Jan 2013 21:16:51 +0100 wenzelm include timing properties in log; build_history_base
Thu, 03 Jan 2013 13:54:45 +0100 wenzelm improved Monitor_Dockable, based on ML_Statistics operations;
Wed, 02 Jan 2013 21:55:57 +0100 wenzelm added standard_frames convenience;
Wed, 02 Jan 2013 21:39:54 +0100 wenzelm some grouping of standard fields;
Wed, 02 Jan 2013 21:02:47 +0100 wenzelm some support for chart drawing;
Wed, 02 Jan 2013 19:23:18 +0100 wenzelm some support for ML statistics content interpretation;
Wed, 02 Jan 2013 16:48:22 +0100 wenzelm ML runtime statistics: read properties from build log;
less more (0) tip