cache_string: store trimmed string value;

--- a/src/Pure/General/xml.scala	Sat Aug 07 23:02:19 2010 +0200
+++ b/src/Pure/General/xml.scala	Sun Aug 08 13:59:57 2010 +0200
@@ -118,7 +118,7 @@
     def cache_string(x: String): String =
       lookup(x) match {
         case Some(y) => y
-        case None => store(x)
+        case None => store(new String(x.toCharArray))  // trim string value
       }
     def cache_props(x: List[(String, String)]): List[(String, String)] =
       if (x.isEmpty) x