# HG changeset patch
# User wenzelm
# Date 1356969414 -3600
# Node ID 561d79d7031f7b6ffdbc868a58d1e1549d4353e9
# Parent  1656248e673f4e00f715b06bb8ddf9925fd45d86
include user counters as well;

diff -r 1656248e673f -r 561d79d7031f src/Pure/ML/ml_statistics_polyml-5.5.0.ML
--- a/src/Pure/ML/ml_statistics_polyml-5.5.0.ML	Mon Dec 31 16:41:51 2012 +0100
+++ b/src/Pure/ML/ml_statistics_polyml-5.5.0.ML	Mon Dec 31 16:56:54 2012 +0100
@@ -32,7 +32,11 @@
       timeGCUser,
       timeNonGCSystem,
       timeNonGCUser,
-      userCounters = _} = PolyML.Statistics.getLocalStats ()
+      userCounters} = PolyML.Statistics.getLocalStats ();
+    val user_counters =
+      Vector.foldri
+        (fn (i, j, res) => ("user_counter" ^ Markup.print_int (i + 1), Markup.print_int j) :: res)
+        [] userCounters;
   in
     [("full_GCs", Markup.print_int gcFullGCs),
      ("partial_GCs", Markup.print_int gcPartialGCs),
@@ -50,7 +54,8 @@
      ("time_GC_system", signed_string_of_real (Time.toReal timeGCSystem)),
      ("time_GC_user", signed_string_of_real (Time.toReal timeGCUser)),
      ("time_non_GC_system", signed_string_of_real (Time.toReal timeNonGCSystem)),
-     ("time_non_GC_user", signed_string_of_real (Time.toReal timeNonGCUser))]
+     ("time_non_GC_user", signed_string_of_real (Time.toReal timeNonGCUser))] @
+    user_counters
   end;
 
 end;