more compact representation of special string values;

--- a/src/Pure/General/properties.scala	Tue Aug 12 12:06:22 2014 +0200
+++ b/src/Pure/General/properties.scala	Tue Aug 12 13:18:17 2014 +0200
@@ -27,7 +27,7 @@
 
     object Int
     {
-      def apply(x: scala.Int): java.lang.String = x.toString
+      def apply(x: scala.Int): java.lang.String = Library.signed_string_of_int(x)
       def unapply(s: java.lang.String): Option[scala.Int] =
         try { Some(Integer.parseInt(s)) }
         catch { case _: NumberFormatException => None }
@@ -35,7 +35,7 @@
 
     object Long
     {
-      def apply(x: scala.Long): java.lang.String = x.toString
+      def apply(x: scala.Long): java.lang.String = Library.signed_string_of_long(x)
       def unapply(s: java.lang.String): Option[scala.Long] =
         try { Some(java.lang.Long.parseLong(s)) }
         catch { case _: NumberFormatException => None }

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

--- a/src/Pure/library.ML	Tue Aug 12 12:06:22 2014 +0200
+++ b/src/Pure/library.ML	Tue Aug 12 13:18:17 2014 +0200
@@ -642,14 +642,14 @@
 
 local
   val zero = ord "0";
-  val small = 10000: int;
-  val small_table = Vector.tabulate (small, Int.toString);
+  val small_int = 10000: int;
+  val small_int_table = Vector.tabulate (small_int, Int.toString);
 in
 
 fun string_of_int i =
   if i < 0 then Int.toString i
   else if i < 10 then chr (zero + i)
-  else if i < small then Vector.sub (small_table, i)
+  else if i < small_int then Vector.sub (small_int_table, i)
   else Int.toString i;
 
 end;

--- a/src/Pure/library.scala	Tue Aug 12 12:06:22 2014 +0200
+++ b/src/Pure/library.scala	Tue Aug 12 13:18:17 2014 +0200
@@ -32,6 +32,33 @@
     error(cat_message(msg1, msg2))
 
 
+  /* integers */
+
+  private val small_int = 10000
+  private lazy val small_int_table =
+  {
+    val array = new Array[String](small_int)
+    for (i <- 0 until small_int) array(i) = i.toString
+    array
+  }
+
+  def is_small_int(s: String): Boolean =
+  {
+    val len = s.length
+    1 <= len && len <= 4 &&
+    s.forall(c => '0' <= c && c <= '9') &&
+    (len == 1 || s(0) != '0')
+  }
+
+  def signed_string_of_long(i: Long): String =
+    if (0 <= i && i < small_int) small_int_table(i.toInt)
+    else i.toString
+
+  def signed_string_of_int(i: Int): String =
+    if (0 <= i && i < small_int) small_int_table(i)
+    else i.toString
+
+
   /* separated chunks */
 
   def separate[A](s: A, list: List[A]): List[A] =