# HG changeset patch # User wenzelm # Date 1594836405 -7200 # Node ID 7b112eedc8598223bf2d38fa2c9003dd0228768b # Parent bc85d93aad23c2d6cb43a721a143afed630f5a85 more robust wrt. experimental changes in Poly/ML; diff -r bc85d93aad23 -r 7b112eedc859 src/Pure/ML/ml_statistics.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 *)