--- 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
--- 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])
}