| Sun, 26 Mar 2023 12:53:53 +0200 |
wenzelm |
clarified signature: more explicit types;
|
file |
diff |
annotate
|
| Sun, 26 Mar 2023 12:41:34 +0200 |
wenzelm |
clarified signature: more explicit types;
|
file |
diff |
annotate
|
| Fri, 24 Feb 2023 20:40:50 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 06 Feb 2023 16:29:19 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 28 Jan 2023 16:08:43 +0100 |
wenzelm |
clarified signature: more explicit types;
|
file |
diff |
annotate
|
| Sat, 28 Jan 2023 15:38:36 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 28 Jan 2023 15:35:43 +0100 |
wenzelm |
clarified signature: more robust field_scale;
|
file |
diff |
annotate
|
| Sat, 28 Jan 2023 15:04:15 +0100 |
wenzelm |
clarified signature: more explicit types;
|
file |
diff |
annotate
|
| Fri, 27 Jan 2023 18:59:48 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 21 Apr 2022 10:03:38 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2022 17:06:10 +0200 |
wenzelm |
clarified formatting, for the sake of scala3;
|
file |
diff |
annotate
|
| Thu, 31 Mar 2022 21:51:19 +0200 |
wenzelm |
tuned: avoid problems with scala3;
|
file |
diff |
annotate
|
| Sat, 27 Nov 2021 14:03:44 +0100 |
wenzelm |
tuned output;
|
file |
diff |
annotate
|
| Sat, 27 Nov 2021 13:55:03 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 17 May 2021 14:54:03 +0200 |
wenzelm |
more uniform use of Properties.Eq.unapply, with slightly changed semantics in boundary cases;
|
file |
diff |
annotate
|
| Sun, 25 Apr 2021 22:33:15 +0200 |
wenzelm |
avoid "exec" to change the winpid;
|
file |
diff |
annotate
|
| Wed, 31 Mar 2021 22:10:56 +0200 |
wenzelm |
tuned signature -- more explicit types;
|
file |
diff |
annotate
|
| Thu, 04 Mar 2021 21:04:27 +0100 |
wenzelm |
clarified signature --- fewer warnings;
|
file |
diff |
annotate
|
| Thu, 04 Mar 2021 15:41:46 +0100 |
wenzelm |
tuned --- fewer warnings;
|
file |
diff |
annotate
|
| Mon, 01 Mar 2021 22:22:12 +0100 |
wenzelm |
tuned --- fewer warnings;
|
file |
diff |
annotate
|
| Sun, 10 Jan 2021 13:04:29 +0100 |
wenzelm |
more informative errors: simplify diagnosis of spurious failures reported by users;
|
file |
diff |
annotate
|
| Sat, 02 Jan 2021 22:22:34 +0100 |
wenzelm |
clarified signature: absorb XZ.Cache into XML.Cache;
|
file |
diff |
annotate
|
| Thu, 10 Sep 2020 21:14:50 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Fri, 28 Aug 2020 16:14:19 +0200 |
wenzelm |
more robust interpretation of data;
|
file |
diff |
annotate
|
| Thu, 27 Aug 2020 12:43:06 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 27 Aug 2020 12:34:10 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 15 Aug 2020 13:45:25 +0200 |
wenzelm |
clarified names;
|
file |
diff |
annotate
|
| Thu, 13 Aug 2020 15:11:30 +0200 |
wenzelm |
support JVM runtime statistics;
|
file |
diff |
annotate
|
| Thu, 13 Aug 2020 12:38:44 +0200 |
wenzelm |
clarified order for GUI;
|
file |
diff |
annotate
|
| Wed, 12 Aug 2020 19:32:45 +0200 |
wenzelm |
support for Poly/ML memory status;
|
file |
diff |
annotate
|
| Wed, 12 Aug 2020 11:26:01 +0200 |
wenzelm |
removed pointless option "ML_statistics": always enabled;
|
file |
diff |
annotate
|
| Fri, 07 Aug 2020 22:57:14 +0200 |
wenzelm |
provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127, otherwise ignored);
|
file |
diff |
annotate
|
| Fri, 07 Aug 2020 22:23:40 +0200 |
wenzelm |
cache props;
|
file |
diff |
annotate
|
| Fri, 07 Aug 2020 22:19:32 +0200 |
wenzelm |
clarified names;
|
file |
diff |
annotate
|
| Fri, 07 Aug 2020 20:19:49 +0200 |
wenzelm |
ML statistics via external process: allows monitoring RTS while ML program sleeps;
|
file |
diff |
annotate
|
| Thu, 16 Jul 2020 11:43:32 +0200 |
wenzelm |
more robust: avoid potential problems with encoding of directory name;
|
file |
diff |
annotate
|
| Wed, 15 Jul 2020 12:43:36 +0200 |
wenzelm |
proper platform path for Windows;
|
file |
diff |
annotate
|
| Wed, 15 Jul 2020 12:04:48 +0200 |
wenzelm |
support for monitoring of external ML process;
|
file |
diff |
annotate
|
| Fri, 27 Mar 2020 22:01:27 +0100 |
wenzelm |
misc tuning based on hints by IntelliJ IDEA;
|
file |
diff |
annotate
|
| Sat, 23 Feb 2019 21:33:09 +0100 |
wenzelm |
more memory fields;
|
file |
diff |
annotate
|
| Wed, 20 Feb 2019 12:10:40 +0100 |
wenzelm |
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
|
file |
diff |
annotate
|
| Wed, 09 May 2018 19:53:37 +0200 |
wenzelm |
record total number of tasks;
|
file |
diff |
annotate
|
| Sat, 03 Mar 2018 21:38:27 +0100 |
wenzelm |
more compact ML_Statistics, to make build_status work with less than 2GB heap;
|
file |
diff |
annotate
|
| Thu, 18 May 2017 14:38:09 +0200 |
wenzelm |
uniform heap_scale;
|
file |
diff |
annotate
|
| Thu, 18 May 2017 13:51:25 +0200 |
wenzelm |
simplified signature;
|
file |
diff |
annotate
|
| Wed, 17 May 2017 22:27:33 +0200 |
wenzelm |
more systematic maximum and average;
|
file |
diff |
annotate
|
| Wed, 17 May 2017 20:52:24 +0200 |
wenzelm |
store processed content instead of somewhat bulky properties;
|
file |
diff |
annotate
|
| Wed, 17 May 2017 14:58:48 +0200 |
wenzelm |
include full ML statistics: max heap size;
|
file |
diff |
annotate
|
| Wed, 17 May 2017 13:47:19 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 13 Apr 2017 12:27:57 +0200 |
wenzelm |
clarified directories;
|
file |
diff |
annotate
| base
|
| 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);
|
file |
diff |
annotate
|
| Sat, 12 Jan 2013 22:14:29 +0100 |
wenzelm |
proper window title;
|
file |
diff |
annotate
|
| Sat, 12 Jan 2013 22:08:38 +0100 |
wenzelm |
add icon for toplevel windows;
|
file |
diff |
annotate
|
| Tue, 08 Jan 2013 21:16:51 +0100 |
wenzelm |
include timing properties in log;
build_history_base
|
file |
diff |
annotate
|
| Thu, 03 Jan 2013 13:54:45 +0100 |
wenzelm |
improved Monitor_Dockable, based on ML_Statistics operations;
|
file |
diff |
annotate
|
| Wed, 02 Jan 2013 21:55:57 +0100 |
wenzelm |
added standard_frames convenience;
|
file |
diff |
annotate
|
| Wed, 02 Jan 2013 21:39:54 +0100 |
wenzelm |
some grouping of standard fields;
|
file |
diff |
annotate
|
| Wed, 02 Jan 2013 21:02:47 +0100 |
wenzelm |
some support for chart drawing;
|
file |
diff |
annotate
|
| Wed, 02 Jan 2013 19:23:18 +0100 |
wenzelm |
some support for ML statistics content interpretation;
|
file |
diff |
annotate
|
| Wed, 02 Jan 2013 16:48:22 +0100 |
wenzelm |
ML runtime statistics: read properties from build log;
|
file |
diff |
annotate
|