author | wenzelm |
Tue, 18 Feb 2014 18:43:31 +0100 | |
changeset 55554 | d77090e07000 |
parent 55553 | 99409ccbe04a |
child 55555 | 9c16317c91d1 |
--- a/src/Pure/PIDE/yxml.scala Tue Feb 18 18:29:02 2014 +0100 +++ b/src/Pure/PIDE/yxml.scala Tue Feb 18 18:43:31 2014 +0100 @@ -33,7 +33,7 @@ def tree(t: XML.Tree): Unit = t match { case XML.Elem(Markup(name, atts), ts) => - s += X; s += Y; s++= name; atts.foreach(attrib); s += X + s += X; s += Y; s ++= name; atts.foreach(attrib); s += X ts.foreach(tree) s += X; s += Y; s += X case XML.Text(text) => s ++= text