# HG changeset patch
# User wenzelm
# Date 1735223901 -3600
# Node ID cd6e187c7c452aec0ade7669954db5b0ce313dab
# Parent  4210fd10e7769d3b423d0f1973d763183c6e0eb1
tuned;

diff -r 4210fd10e776 -r cd6e187c7c45 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Thu Dec 26 15:24:21 2024 +0100
+++ b/src/Pure/General/symbol.scala	Thu Dec 26 15:38:21 2024 +0100
@@ -25,18 +25,17 @@
   val space_char = ' '
   val space = " "
 
-  private val static_spaces_length = 4000
-  private val static_spaces = space * static_spaces_length
+  private val static_spaces = space * 4000
 
   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)
+    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 == 0) ""
-    else if (n < static_spaces_length) static_spaces.substring(0, n)
+    else if (n < static_spaces.length) static_spaces.substring(0, n)
     else space * n
   }