# HG changeset patch
# User wenzelm
# Date 1731327355 -3600
# Node ID 0ccfc82fff57d2169498d612282b8289cca386cf
# Parent  257ec066b36037c7c3e372a4a48ceded20506331
minor performance tuning: avoid duplication of Symbol.spaces (e.g. from Pretty.formatted);

diff -r 257ec066b360 -r 0ccfc82fff57 src/Pure/General/cache.scala
--- a/src/Pure/General/cache.scala	Mon Nov 11 12:47:51 2024 +0100
+++ b/src/Pure/General/cache.scala	Mon Nov 11 13:15:55 2024 +0100
@@ -56,6 +56,7 @@
     else if (x == "true") "true"
     else if (x == "false") "false"
     else if (x == "0.0") "0.0"
+    else if (Symbol.is_static_spaces(x)) Symbol.spaces(x.length)
     else if (Library.is_small_int(x)) Library.signed_string_of_int(Integer.parseInt(x))
     else {
       lookup(x) match {
diff -r 257ec066b360 -r 0ccfc82fff57 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Mon Nov 11 12:47:51 2024 +0100
+++ b/src/Pure/General/symbol.scala	Mon Nov 11 13:15:55 2024 +0100
@@ -25,11 +25,18 @@
   val space_char = ' '
   val space = " "
 
-  private val static_spaces = space * 4000
+  private val static_spaces_length = 4000
+  private val static_spaces = space * static_spaces_length
+
+  def is_static_spaces(s: String): Boolean = {
+    val n = s.length
+    n == 0 || n <= static_spaces_length && s(0) == space_char && s.forall(_ == space_char)
+  }
 
   def spaces(n: Int): String = {
     require(n >= 0, "negative spaces")
-    if (n < static_spaces.length) static_spaces.substring(0, n)
+    if (n == 0) ""
+    else if (n < static_spaces_length) static_spaces.substring(0, n)
     else space * n
   }