# HG changeset patch
# User wenzelm
# Date 1283029104 -7200
# Node ID f3221fd64426da91422befa9aa253a6f04c901fd
# Parent  d95522496593419c8d9d70dd675b330d74517db0
XML.Cache: intern property keys once and for all (again);

diff -r d95522496593 -r f3221fd64426 src/Pure/General/xml.scala
--- a/src/Pure/General/xml.scala	Sat Aug 28 20:24:41 2010 +0200
+++ b/src/Pure/General/xml.scala	Sat Aug 28 22:58:24 2010 +0200
@@ -112,7 +112,7 @@
         else
           lookup(x) match {
             case Some(y) => y
-            case None => store(x.map(p => (cache_string(p._1), cache_string(p._2))))
+            case None => store(x.map(p => (cache_string(p._1).intern, cache_string(p._2))))
           }
       def cache_markup(x: Markup): Markup =
         lookup(x) match {