# HG changeset patch
# User wenzelm
# Date 1281268797 -7200
# Node ID 501dcbd8f399a3c4d406a7f234348fe66ede180a
# Parent  00b72526dc64efe37569f908a5bd01c7490924f7
cache_string: store trimmed string value;

diff -r 00b72526dc64 -r 501dcbd8f399 src/Pure/General/xml.scala
--- 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