more robust wrt. experimental changes in Poly/ML;
--- a/src/Pure/ML/ml_statistics.ML Wed Jul 15 17:10:26 2020 +0200
+++ b/src/Pure/ML/ml_statistics.ML Wed Jul 15 20:06:45 2020 +0200
@@ -50,6 +50,8 @@
(* get properties *)
+local
+
fun make_properties
{gcFullGCs,
gcPartialGCs,
@@ -73,7 +75,7 @@
timeNonGCReal,
timeNonGCSystem,
timeNonGCUser,
- userCounters} =
+ userCounters, ...} =
let
val tasks_ready = Vector.sub (userCounters, 0);
val tasks_pending = Vector.sub (userCounters, 1);
@@ -117,12 +119,16 @@
("time_GC", print_real (Time.toReal timeGCSystem + Time.toReal timeGCUser))]
end;
+in
+
fun get () =
make_properties (PolyML.Statistics.getLocalStats ());
fun get_external pid =
make_properties (PolyML.Statistics.getRemoteStats pid);
+end;
+
(* monitor process *)