# HG changeset patch
# User wenzelm
# Date 1282122508 -7200
# Node ID 1dd4f545ac24e559552b8a0294f7c5a9f7e6ffe5
# Parent  e498dc2eb57608c8bb41aa061a105673e0838126
tuned;

diff -r e498dc2eb576 -r 1dd4f545ac24 src/Pure/General/yxml.scala
--- a/src/Pure/General/yxml.scala	Wed Aug 18 11:02:47 2010 +0200
+++ b/src/Pure/General/yxml.scala	Wed Aug 18 11:08:28 2010 +0200
@@ -85,7 +85,7 @@
     /* stack operations */
 
     def buffer(): ListBuffer[XML.Tree] = new ListBuffer[XML.Tree]
-    var stack: List[(Markup, ListBuffer[XML.Tree])] = List((Markup("", Nil), buffer()))
+    var stack: List[(Markup, ListBuffer[XML.Tree])] = List((Markup.Empty, buffer()))
 
     def add(x: XML.Tree)
     {
@@ -101,7 +101,7 @@
     def pop()
     {
       (stack: @unchecked) match {
-        case ((Markup("", _), _) :: _) => err_unbalanced("")
+        case ((Markup.Empty, _) :: _) => err_unbalanced("")
         case ((markup, body) :: pending) =>
           stack = pending
           add(XML.Elem(markup, body.toList))
@@ -122,7 +122,7 @@
       }
     }
     stack match {
-      case List((Markup("", _), body)) => body.toList
+      case List((Markup.Empty, body)) => body.toList
       case (Markup(name, _), _) :: _ => err_unbalanced(name)
     }
   }