src/Pure/ML/ml_statistics.scala
Fri, 07 Aug 2020 22:23:40 +0200 wenzelm cache props;
Fri, 07 Aug 2020 22:19:32 +0200 wenzelm clarified names;
Fri, 07 Aug 2020 20:19:49 +0200 wenzelm ML statistics via external process: allows monitoring RTS while ML program sleeps;
Thu, 16 Jul 2020 11:43:32 +0200 wenzelm more robust: avoid potential problems with encoding of directory name;
Wed, 15 Jul 2020 12:43:36 +0200 wenzelm proper platform path for Windows;
Wed, 15 Jul 2020 12:04:48 +0200 wenzelm support for monitoring of external ML process;
Fri, 27 Mar 2020 22:01:27 +0100 wenzelm misc tuning based on hints by IntelliJ IDEA;
Sat, 23 Feb 2019 21:33:09 +0100 wenzelm more memory fields;
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