# HG changeset patch
# User wenzelm
# Date 1690280851 -7200
# Node ID 14ceb9a51e97f292a5e253feff2f1b904896ed62
# Parent  c32b8d5a9e072da068a20a2eeea838e610bb81c4
clarified statistics;

diff -r c32b8d5a9e07 -r 14ceb9a51e97 src/Pure/Tools/profiling.scala
--- a/src/Pure/Tools/profiling.scala	Mon Jul 24 22:53:18 2023 +0200
+++ b/src/Pure/Tools/profiling.scala	Tue Jul 25 12:27:31 2023 +0200
@@ -109,8 +109,8 @@
 
     val header0: List[String] =
       List(
-        "theories",
-        "garbage_theories%",
+        "named_theories",
+        "total_theories",
         "locales",
         "locale_thms",
         "global_thms",
@@ -142,8 +142,12 @@
     val types_size: Space = Space.zero,
     val spaces_size: Space = Space.zero
   ) {
-    def garbage_theories_percentage: Percentage =
-      percentage(garbage_theories, theories + garbage_theories)
+    private def print_total_theories: String =
+      if (theories == 0) "0"
+      else {
+        val x = (theories + garbage_theories).toDouble / theories
+        String.format(Locale.ROOT, "%.1f", x.asInstanceOf[AnyRef])
+      }
 
     private def size_percentage(space: Space): Percentage =
       percentage_space(space, heap_size)
@@ -154,7 +158,7 @@
     val fields0: List[Any] =
       List(
         theories,
-        garbage_theories_percentage.toString,
+        print_total_theories,
         locales,
         locale_thms,
         global_thms,
diff -r c32b8d5a9e07 -r 14ceb9a51e97 src/Tools/profiling.ML
--- a/src/Tools/profiling.ML	Mon Jul 24 22:53:18 2023 +0200
+++ b/src/Tools/profiling.ML	Tue Jul 25 12:27:31 2023 +0200
@@ -116,7 +116,7 @@
           types = base_types, spaces = base_spaces} = session_content base_thys;
 
     val n = length loaded_thys;
-    val m = length loaded_context_thys - n;
+    val m = (case length loaded_context_thys of 0 => 0 | l => l - n);
   in
     {theories = n,
      garbage_theories = m,