# HG changeset patch
# User wenzelm
# Date 1594670838 -7200
# Node ID b7cec26e41d1eabf2293c08888c5086227e1a814
# Parent  eece87547736b4a7a4648620d26c22a31df9cc2f
clarified modules: ML_Statistics within bootstrap environment;

diff -r eece87547736 -r b7cec26e41d1 src/Pure/ML/ml_statistics.ML
--- a/src/Pure/ML/ml_statistics.ML	Mon Jul 13 21:20:36 2020 +0200
+++ b/src/Pure/ML/ml_statistics.ML	Mon Jul 13 22:07:18 2020 +0200
@@ -6,12 +6,29 @@
 
 signature ML_STATISTICS =
 sig
-  val get: unit -> Properties.T
+  val get: unit -> (string * string) list
 end;
 
 structure ML_Statistics: ML_STATISTICS =
 struct
 
+(* print *)
+
+fun print_int x = if x < 0 then "-" ^ Int.toString (~ x) else Int.toString x;
+
+fun print_real0 x =
+  let val s = Real.fmt (StringCvt.GEN NONE) x in
+    (case String.fields (fn c => c = #".") s of
+      [a, b] => if List.all (fn c => c = #"0") (String.explode b) then a else s
+    | _ => s)
+  end;
+
+fun print_real x =
+  if x < 0.0 then "-" ^ print_real0 (~ x) else print_real0 x;
+
+
+(* get *)
+
 fun get () =
   let
     val
@@ -40,29 +57,29 @@
       userCounters} = PolyML.Statistics.getLocalStats ();
     val user_counters =
       Vector.foldri
-        (fn (i, j, res) => ("user_counter" ^ Value.print_int i, Value.print_int j) :: res)
+        (fn (i, j, res) => ("user_counter" ^ print_int i, print_int j) :: res)
         [] userCounters;
   in
-    [("full_GCs", Value.print_int gcFullGCs),
-     ("partial_GCs", Value.print_int gcPartialGCs),
-     ("share_passes", Value.print_int gcSharePasses),
-     ("size_allocation", Value.print_int sizeAllocation),
-     ("size_allocation_free", Value.print_int sizeAllocationFree),
-     ("size_code", Value.print_int sizeCode),
-     ("size_heap", Value.print_int sizeHeap),
-     ("size_heap_free_last_full_GC", Value.print_int sizeHeapFreeLastFullGC),
-     ("size_heap_free_last_GC", Value.print_int sizeHeapFreeLastGC),
-     ("size_stacks", Value.print_int sizeStacks),
-     ("threads_in_ML", Value.print_int threadsInML),
-     ("threads_total", Value.print_int threadsTotal),
-     ("threads_wait_condvar", Value.print_int threadsWaitCondVar),
-     ("threads_wait_IO", Value.print_int threadsWaitIO),
-     ("threads_wait_mutex", Value.print_int threadsWaitMutex),
-     ("threads_wait_signal", Value.print_int threadsWaitSignal),
-     ("time_elapsed", Value.print_real (Time.toReal timeNonGCReal)),
-     ("time_elapsed_GC", Value.print_real (Time.toReal timeGCReal)),
-     ("time_CPU", Value.print_real (Time.toReal timeNonGCSystem + Time.toReal timeNonGCUser)),
-     ("time_GC", Value.print_real (Time.toReal timeGCSystem + Time.toReal timeGCUser))] @
+    [("full_GCs", print_int gcFullGCs),
+     ("partial_GCs", print_int gcPartialGCs),
+     ("share_passes", print_int gcSharePasses),
+     ("size_allocation", print_int sizeAllocation),
+     ("size_allocation_free", print_int sizeAllocationFree),
+     ("size_code", print_int sizeCode),
+     ("size_heap", print_int sizeHeap),
+     ("size_heap_free_last_full_GC", print_int sizeHeapFreeLastFullGC),
+     ("size_heap_free_last_GC", print_int sizeHeapFreeLastGC),
+     ("size_stacks", print_int sizeStacks),
+     ("threads_in_ML", print_int threadsInML),
+     ("threads_total", print_int threadsTotal),
+     ("threads_wait_condvar", print_int threadsWaitCondVar),
+     ("threads_wait_IO", print_int threadsWaitIO),
+     ("threads_wait_mutex", print_int threadsWaitMutex),
+     ("threads_wait_signal", print_int threadsWaitSignal),
+     ("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))] @
     user_counters
   end;
 
diff -r eece87547736 -r b7cec26e41d1 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Jul 13 21:20:36 2020 +0200
+++ b/src/Pure/ROOT.ML	Mon Jul 13 22:07:18 2020 +0200
@@ -114,8 +114,6 @@
 ML_file "ML/exn_properties.ML";
 ML_file_no_debug "ML/exn_debugger.ML";
 
-ML_file "ML/ml_statistics.ML";
-
 ML_file "Concurrent/thread_data_virtual.ML";
 ML_file "Concurrent/isabelle_thread.ML";
 ML_file "Concurrent/single_assignment.ML";
diff -r eece87547736 -r b7cec26e41d1 src/Pure/ROOT0.ML
--- a/src/Pure/ROOT0.ML	Mon Jul 13 21:20:36 2020 +0200
+++ b/src/Pure/ROOT0.ML	Mon Jul 13 22:07:18 2020 +0200
@@ -1,5 +1,7 @@
 (*** Isabelle/Pure bootstrap: initial setup ***)
 
+ML_file "ML/ml_statistics.ML";
+
 ML_file "General/exn.ML";
 ML_file "General/output_primitives.ML";