| 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,