src/Pure/Tools/profiling.scala
changeset 78958 c125f75a5144
parent 78452 14ceb9a51e97
child 79095 3bdd3cf5f5e0
--- a/src/Pure/Tools/profiling.scala	Sun Nov 12 12:33:22 2023 +0100
+++ b/src/Pure/Tools/profiling.scala	Sun Nov 12 12:34:04 2023 +0100
@@ -97,7 +97,7 @@
         locales = session.locales,
         locale_thms = session.locale_thms,
         global_thms = session.global_thms,
-        heap_size = Space.bytes(store.the_heap(session_name).file.length),
+        heap_size = File.space(store.the_heap(session_name)),
         thys_id_size = session.sizeof_thys_id,
         thms_id_size = session.sizeof_thms_id,
         terms_size = session.sizeof_terms,