src/Pure/General/yxml.scala

--- a/src/Pure/General/yxml.scala	Sat Aug 07 21:22:39 2010 +0200
+++ b/src/Pure/General/yxml.scala	Sat Aug 07 22:09:52 2010 +0200
@@ -64,7 +64,7 @@
     /* stack operations */
 
     def buffer(): ListBuffer[XML.Tree] = new ListBuffer[XML.Tree]
-    var stack: List[((String, XML.Attributes), ListBuffer[XML.Tree])] = List((("", Nil), buffer()))
+    var stack: List[(Markup, ListBuffer[XML.Tree])] = List((Markup("", Nil), buffer()))
 
     def add(x: XML.Tree)
     {
@@ -74,15 +74,16 @@
     def push(name: String, atts: XML.Attributes)
     {
       if (name == "") err_element()
-      else stack = ((name, atts), buffer()) :: stack
+      else stack = (Markup(name, atts), buffer()) :: stack
     }
 
     def pop()
     {
       (stack: @unchecked) match {
-        case ((("", _), _) :: _) => err_unbalanced("")
-        case (((name, atts), body) :: pending) =>
-          stack = pending; add(XML.Elem(name, atts, body.toList))
+        case ((Markup("", _), _) :: _) => err_unbalanced("")
+        case ((markup, body) :: pending) =>
+          stack = pending
+          add(XML.Elem(markup, body.toList))
       }
     }
 
@@ -100,8 +101,8 @@
       }
     }
     stack match {
-      case List((("", _), body)) => body.toList
-      case ((name, _), _) :: _ => err_unbalanced(name)
+      case List((Markup("", _), body)) => body.toList
+      case (Markup(name, _), _) :: _ => err_unbalanced(name)
     }
   }
 
@@ -116,7 +117,7 @@
   /* failsafe parsing */
 
   private def markup_failsafe(source: CharSequence) =
-    XML.Elem (Markup.MALFORMED, Nil,
+    XML.Elem (Markup(Markup.MALFORMED, Nil),
       List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>"))))
 
   def parse_body_failsafe(source: CharSequence): List[XML.Tree] =