def memory_status(): Memory_Status = { val heap_size = Space.bytes(Runtime.getRuntime.totalMemory()) val heap_free = Space.bytes(Runtime.getRuntime.freeMemory())
Memory_Status(heap_size, heap_free)
}
/* JVM statistics */
def jvm_statistics(): Properties.T = { val status = memory_status() val threads = Thread.activeCount() val workers = Isabelle_Thread.pool.getPoolSize val workers_active = Isabelle_Thread.pool.getActiveCount
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.