# HG changeset patch
# User wenzelm
# Date 1283159366 -7200
# Node ID 7634e3f105764e03149e701f4015930ec52893c8
# Parent  0f861635949db38595d852442486512631a2d15a
tuned;

diff -r 0f861635949d -r 7634e3f10576 src/Pure/General/xml.scala
--- a/src/Pure/General/xml.scala	Mon Aug 30 10:38:28 2010 +0200
+++ b/src/Pure/General/xml.scala	Mon Aug 30 11:09:26 2010 +0200
@@ -102,17 +102,19 @@
         x
       }
 
+      def trim_bytes(s: String): String = new String(s.toCharArray)
+
       def cache_string(x: String): String =
         lookup(x) match {
           case Some(y) => y
-          case None => store(new String(x.toCharArray))  // trim string value
+          case None => store(trim_bytes(x))
         }
       def cache_props(x: List[(String, String)]): List[(String, String)] =
         if (x.isEmpty) x
         else
           lookup(x) match {
             case Some(y) => y
-            case None => store(x.map(p => (cache_string(p._1).intern, cache_string(p._2))))
+            case None => store(x.map(p => (trim_bytes(p._1).intern, cache_string(p._2))))
           }
       def cache_markup(x: Markup): Markup =
         lookup(x) match {