# HG changeset patch
# User wenzelm
# Date 1294672036 -3600
# Node ID 7a4138cb46dbbede25b4fd889c1866155f43247f
# Parent  a2ad5b8240510de04096fe0e4bd267654845ca67
tuned string_of_int to avoid allocation for small integers;

diff -r a2ad5b824051 -r 7a4138cb46db src/Pure/library.ML
--- a/src/Pure/library.ML	Mon Jan 10 15:45:46 2011 +0100
+++ b/src/Pure/library.ML	Mon Jan 10 16:07:16 2011 +0100
@@ -642,7 +642,19 @@
   in implode (map chrof (radixpand (base, num))) end;
 
 
-val string_of_int = Int.toString;
+local
+  val zero = ord "0";
+  val small = 10000;
+  val small_table = Vector.tabulate (small, 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 Int.toString i;
+
+end;
 
 fun signed_string_of_int i =
   if i < 0 then "-" ^ string_of_int (~ i) else string_of_int i;