# HG changeset patch
# User wenzelm
# Date 1232377384 -3600
# Node ID 4773c5c994dc72dfcf1f51dfd04f49a0d989007d
# Parent  7de51bcbf15e942ef20f8601c01a047c018d052d
intern names of elements and attributes;

diff -r 7de51bcbf15e -r 4773c5c994dc src/Pure/General/yxml.scala
--- a/src/Pure/General/yxml.scala	Mon Jan 19 13:38:59 2009 +0100
+++ b/src/Pure/General/yxml.scala	Mon Jan 19 16:03:04 2009 +0100
@@ -59,7 +59,7 @@
     val s = source.toString
     val i = s.indexOf('=')
     if (i <= 0) err_attribute()
-    (s.substring(0, i), s.substring(i + 1))
+    (s.substring(0, i).intern, s.substring(i + 1))
   }
 
 
@@ -91,7 +91,7 @@
       if (chunk == Y_string) pop()
       else {
         chunks(Y, chunk).toList match {
-          case "" :: name :: atts => push(name.toString, atts.map(parse_attrib))
+          case "" :: name :: atts => push(name.toString.intern, atts.map(parse_attrib))
           case txts => for (txt <- txts) add(XML.Text(txt.toString))
         }
       }