more detailed profiling including "names";
avoid overlapping results;

--- a/src/Pure/Tools/profiling.scala	Thu Nov 30 13:35:17 2023 +0100
+++ b/src/Pure/Tools/profiling.scala	Thu Nov 30 16:33:00 2023 +0100
@@ -39,6 +39,7 @@
     sizeof_thms_id: Space = Space.zero,
     sizeof_terms: Space = Space.zero,
     sizeof_types: Space = Space.zero,
+    sizeof_names: Space = Space.zero,
     sizeof_spaces: Space = Space.zero)
 
   object Statistics {
@@ -49,10 +50,10 @@
     private val decode_result: XML.Decode.T[Session_Statistics] =
       (body: XML.Body) =>
         {
-          val (a, (b, (c, (d, (e, (f, (g, (h, (i, j))))))))) = {
+          val (a, (b, (c, (d, (e, (f, (g, (h, (i, (j, k)))))))))) = {
             import XML.Decode._
             pair(int, pair(int, pair(int, pair(int, pair(int,
-              pair(long, pair(long, pair(long, pair(long, long)))))))))(body)
+              pair(long, pair(long, pair(long, pair(long, pair(long, long))))))))))(body)
           }
           Session_Statistics(
             theories = a,
@@ -64,7 +65,8 @@
             sizeof_thms_id = Space.bytes(g),
             sizeof_terms = Space.bytes(h),
             sizeof_types = Space.bytes(i),
-            sizeof_spaces = Space.bytes(j))
+            sizeof_names = Space.bytes(j),
+            sizeof_spaces = Space.bytes(k))
         }
 
     def make(
@@ -102,6 +104,7 @@
         thms_id_size = session.sizeof_thms_id,
         terms_size = session.sizeof_terms,
         types_size = session.sizeof_types,
+        names_size = session.sizeof_names,
         spaces_size = session.sizeof_spaces)
     }
 
@@ -121,6 +124,7 @@
         "thms_id_size%",
         "terms_size%",
         "types_size%",
+        "names_size%",
         "spaces_size%")
 
     def header: List[String] =
@@ -140,6 +144,7 @@
     val thms_id_size: Space = Space.zero,
     val terms_size: Space = Space.zero,
     val types_size: Space = Space.zero,
+    val names_size: Space = Space.zero,
     val spaces_size: Space = Space.zero
   ) {
     private def print_total_theories: String =
@@ -169,6 +174,7 @@
         size_percentage(thms_id_size).toString,
         size_percentage(terms_size).toString,
         size_percentage(types_size).toString,
+        size_percentage(names_size).toString,
         size_percentage(spaces_size).toString)
 
     def fields: List[Any] =
@@ -190,6 +196,7 @@
             thms_id_size = other.cumulative.thms_id_size + thms_id_size,
             terms_size = other.cumulative.terms_size + terms_size,
             types_size = other.cumulative.types_size + types_size,
+            names_size = other.cumulative.names_size + names_size,
             spaces_size = other.cumulative.spaces_size + spaces_size)
       }
 

--- a/src/Tools/profiling.ML	Thu Nov 30 13:35:17 2023 +0100
+++ b/src/Tools/profiling.ML	Thu Nov 30 16:33:00 2023 +0100
@@ -21,6 +21,7 @@
     sizeof_thms_id: int,
     sizeof_terms: int,
     sizeof_types: int,
+    sizeof_names: int,
     sizeof_spaces: int}
   val session_statistics: string list -> session_statistics
   val main: unit -> unit
@@ -76,8 +77,14 @@
         Locale.locale_space,
         Attrib.attribute_space o Context.Theory,
         Method.method_space o Context.Theory];
-  in {thys_id = thys_id, thms_id = thms_id, terms = terms, types = types, spaces = spaces} end;
+     val names = maps Name_Space.get_names spaces;
+  in
+    {thys_id = thys_id, thms_id = thms_id, terms = terms,
+      types = types, names = names, spaces = spaces}
+  end;
 
+fun sizeof1_diff (a, b) = ML_Heap.sizeof1 a - ML_Heap.sizeof1 b;
+fun sizeof_list_diff (a, b) = ML_Heap.sizeof_list a - ML_Heap.sizeof_list b;
 fun sizeof_diff (a, b) = ML_Heap.sizeof a - ML_Heap.sizeof b;
 
 
@@ -93,6 +100,7 @@
   sizeof_thms_id: int,
   sizeof_terms: int,
   sizeof_types: int,
+  sizeof_names: int,
   sizeof_spaces: int};
 
 fun session_statistics theories : session_statistics =
@@ -111,9 +119,9 @@
     val base_thys = filter_out theories_member all_thys;
 
     val {thys_id = all_thys_id, thms_id = all_thms_id, terms = all_terms,
-          types = all_types, spaces = all_spaces} = session_content all_thys;
+          types = all_types, names = all_names, spaces = all_spaces} = session_content all_thys;
     val {thys_id = base_thys_id, thms_id = base_thms_id, terms = base_terms,
-          types = base_types, spaces = base_spaces} = session_content base_thys;
+          types = base_types, names = base_names, spaces = base_spaces} = session_content base_thys;
 
     val n = length loaded_thys;
     val m = (case length loaded_context_thys of 0 => 0 | l => l - n);
@@ -123,11 +131,22 @@
      locales = Integer.sum (map (length o locales) loaded_thys),
      locale_thms = Integer.sum (map (length o locales_thms) loaded_thys),
      global_thms = Integer.sum (map (length o global_thms) loaded_thys),
-     sizeof_thys_id = sizeof_diff (all_thys_id, base_thys_id),
-     sizeof_thms_id = sizeof_diff (all_thms_id, base_thms_id),
-     sizeof_terms = sizeof_diff (all_terms, base_terms),
-     sizeof_types = sizeof_diff (all_types, base_types),
-     sizeof_spaces = sizeof_diff (all_spaces, base_spaces)}
+     sizeof_thys_id =
+      sizeof1_diff ((all_thys_id, all_thms_id), (base_thys_id, all_thms_id)) -
+        sizeof_list_diff (all_thys_id, base_thys_id),
+     sizeof_thms_id =
+      sizeof1_diff ((all_thms_id, all_thys_id), (base_thms_id, all_thys_id)) -
+        sizeof_list_diff (all_thms_id, base_thms_id),
+     sizeof_terms =
+      sizeof1_diff ((all_terms, all_types, all_names), (base_terms, all_types, all_names)) -
+        sizeof_list_diff (all_terms, base_terms),
+     sizeof_types =
+      sizeof1_diff ((all_types, all_names), (base_types, all_names)) -
+        sizeof_list_diff (all_types, base_types),
+     sizeof_spaces =
+      sizeof1_diff ((all_spaces, all_names), (base_spaces, all_names)) -
+        sizeof_list_diff (all_spaces, base_spaces),
+     sizeof_names = sizeof_diff (all_names, base_names)}
   end;
 
 
@@ -148,9 +167,12 @@
        sizeof_thms_id = g,
        sizeof_terms = h,
        sizeof_types = i,
-       sizeof_spaces = j} => ((a, (b, (c, (d, (e, (f, (g, (h, (i, j))))))))))) #>
-  let open XML.Encode
-  in pair int (pair int (pair int (pair int (pair int (pair int (pair int (pair int (pair int int)))))))) end;
+       sizeof_names = j,
+       sizeof_spaces = k} => ((a, (b, (c, (d, (e, (f, (g, (h, (i, (j, k)))))))))))) #>
+  let open XML.Encode in
+    pair int (pair int (pair int (pair int (pair int (pair int (pair int
+      (pair int (pair int (pair int int)))))))))
+  end;
 
 in