diff -r 932b2a7139e2 -r c125f75a5144 src/Pure/Tools/profiling.scala --- 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,