src/Pure/System/java_statistics.scala
changeset 73164 e2132e1553a9
parent 72250 13976f92a2d0
child 75393 87ebf5a50283
equal deleted inserted replaced
73163:624c2b98860a 73164:e2132e1553a9
    19   }
    19   }
    20 
    20 
    21   def memory_status(): Memory_Status =
    21   def memory_status(): Memory_Status =
    22   {
    22   {
    23     val heap_size = Runtime.getRuntime.totalMemory()
    23     val heap_size = Runtime.getRuntime.totalMemory()
    24     val heap_used = heap_size - Runtime.getRuntime.freeMemory()
    24     val heap_free = Runtime.getRuntime.freeMemory()
    25     Memory_Status(heap_size, heap_used)
    25     Memory_Status(heap_size, heap_free)
    26   }
    26   }
    27 
    27 
    28 
    28 
    29   /* JVM statistics */
    29   /* JVM statistics */
    30 
    30