--- a/src/Pure/ML/ml_statistics_polyml-5.5.0.ML Wed Nov 28 19:19:39 2012 +0100
+++ b/src/Pure/ML/ml_statistics_polyml-5.5.0.ML Thu Nov 29 10:45:25 2012 +0100
@@ -6,15 +6,12 @@
signature ML_STATISTICS =
sig
- val enabled: bool Unsynchronized.ref
val get: unit -> Properties.T
end;
structure ML_Statistics: ML_STATISTICS =
struct
-val enabled = Unsynchronized.ref false;
-
fun get () =
let
val
@@ -37,8 +34,7 @@
timeNonGCUser,
userCounters = _} = PolyML.Statistics.getLocalStats ()
in
- [("now", signed_string_of_real (Time.toReal (Time.now ()))),
- ("full_GCs", Markup.print_int gcFullGCs),
+ [("full_GCs", Markup.print_int gcFullGCs),
("partial_GCs", Markup.print_int gcPartialGCs),
("size_allocation", Markup.print_int sizeAllocation),
("size_allocation_free", Markup.print_int sizeAllocationFree),