minor performance tuning: avoid duplication of Symbol.spaces (e.g. from Pretty.formatted);

--- 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 {

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