# 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 {