--- a/src/Pure/PIDE/xml.scala Tue Aug 12 12:06:22 2014 +0200
+++ b/src/Pure/PIDE/xml.scala Tue Aug 12 13:18:17 2014 +0200
@@ -150,12 +150,17 @@
private def trim_bytes(s: String): String = new String(s.toCharArray)
private def cache_string(x: String): String =
- lookup(x) match {
- case Some(y) => y
- case None =>
- val z = trim_bytes(x)
- if (z.length > max_string) z else store(z)
- }
+ if (x == "true") "true"
+ else if (x == "false") "false"
+ else if (x == "0.0") "0.0"
+ else if (Library.is_small_int(x)) Library.signed_string_of_int(Integer.parseInt(x))
+ else
+ lookup(x) match {
+ case Some(y) => y
+ case None =>
+ val z = trim_bytes(x)
+ if (z.length > max_string) z else store(z)
+ }
private def cache_props(x: Properties.T): Properties.T =
if (x.isEmpty) x
else
@@ -214,9 +219,9 @@
/* atomic values */
- def long_atom(i: Long): String = i.toString
+ def long_atom(i: Long): String = Library.signed_string_of_long(i)
- def int_atom(i: Int): String = i.toString
+ def int_atom(i: Int): String = Library.signed_string_of_int(i)
def bool_atom(b: Boolean): String = if (b) "1" else "0"