# HG changeset patch
# User wenzelm
# Date 1623230502 -7200
# Node ID 014b944f4972cf8489756fc05ca225d9135ac59b
# Parent  9134ae401ad50316f2956d641d927f234c96cad4
tuned messages;

diff -r 9134ae401ad5 -r 014b944f4972 src/Pure/ML/ml_profiling.ML
--- a/src/Pure/ML/ml_profiling.ML	Wed Jun 09 10:58:28 2021 +0200
+++ b/src/Pure/ML/ml_profiling.ML	Wed Jun 09 11:21:42 2021 +0200
@@ -43,7 +43,7 @@
 fun print_entry count name =
   let
     val c = string_of_int count;
-    val prefix = Symbol.spaces (Int.max (0, 10 - size c));
+    val prefix = Symbol.spaces (Int.max (0, 12 - size c));
   in prefix ^ c ^ " " ^ name end;
 
 fun profile "" f x = f x
diff -r 9134ae401ad5 -r 014b944f4972 src/Pure/ML/ml_profiling.scala
--- a/src/Pure/ML/ml_profiling.scala	Wed Jun 09 10:58:28 2021 +0200
+++ b/src/Pure/ML/ml_profiling.scala	Wed Jun 09 11:21:42 2021 +0200
@@ -19,7 +19,7 @@
     def clean_name: Entry = copy(name = """-?\(\d+\).*$""".r.replaceAllIn(name, ""))
 
     def print: String =
-      String.format(Locale.ROOT, "%10d %s",
+      String.format(Locale.ROOT, "%12d %s",
         count.asInstanceOf[AnyRef], name.asInstanceOf[AnyRef])
   }