changeset 52890 | 36e2c0c308eb |
parent 51987 | 7d8e0e3c553b |
child 55618 | 995162143ef4 |
--- a/src/Pure/PIDE/xml.scala Wed Aug 07 13:46:32 2013 +0200 +++ b/src/Pure/PIDE/xml.scala Wed Aug 07 14:13:59 2013 +0200 @@ -22,6 +22,9 @@ sealed abstract class Tree { override def toString = string_of_tree(this) } case class Elem(markup: Markup, body: List[Tree]) extends Tree + { + def name: String = markup.name + } case class Text(content: String) extends Tree def elem(name: String, body: List[Tree]) = Elem(Markup(name, Nil), body)