src/Pure/General/cache.scala
changeset 81429 0ccfc82fff57
parent 75393 87ebf5a50283
child 81433 c3793899b880
--- 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 {