# HG changeset patch
# User wenzelm
# Date 1597223234 -7200
# Node ID f40200b5bb3cc97e953fe71aff51b90eb51347df
# Parent  c500f6c86e869e66a42957629d6cadffd2d25a4a
support for GC state;

diff -r c500f6c86e86 -r f40200b5bb3c src/Pure/ML/ml_statistics.ML
--- a/src/Pure/ML/ml_statistics.ML	Tue Aug 11 19:01:31 2020 +0200
+++ b/src/Pure/ML/ml_statistics.ML	Wed Aug 12 11:07:14 2020 +0200
@@ -75,7 +75,8 @@
     timeNonGCReal,
     timeNonGCSystem,
     timeNonGCUser,
-    userCounters, ...} =
+    userCounters,
+    gcState = gc_state} =
   let
     val tasks_ready = Vector.sub (userCounters, 0);
     val tasks_pending = Vector.sub (userCounters, 1);
@@ -86,6 +87,13 @@
     val workers_total = Vector.sub (userCounters, 5);
     val workers_active = Vector.sub (userCounters, 6);
     val workers_waiting = Vector.sub (userCounters, 7);
+    val gc_percent =
+      (case gc_state of
+        PolyML.Statistics.MLCode => 0
+      | PolyML.Statistics.MinorGC p => p + 1
+      | PolyML.Statistics.MajorGC p => p + 1
+      | PolyML.Statistics.GCSharing p => p + 1
+      | PolyML.Statistics.OtherState p => p + 1);
   in
     [("now", print_real (Time.toReal (Time.now ()))),
      ("tasks_ready", print_int tasks_ready),
@@ -116,7 +124,8 @@
      ("time_elapsed", print_real (Time.toReal timeNonGCReal)),
      ("time_elapsed_GC", print_real (Time.toReal timeGCReal)),
      ("time_CPU", print_real (Time.toReal timeNonGCSystem + Time.toReal timeNonGCUser)),
-     ("time_GC", print_real (Time.toReal timeGCSystem + Time.toReal timeGCUser))]
+     ("time_GC", print_real (Time.toReal timeGCSystem + Time.toReal timeGCUser)),
+     ("GC_percent", print_int gc_percent)]
   end;
 
 in