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 {