| changeset 38267 | e50c283dd125 |
| parent 38263 | 11c2b8d1fde0 |
| child 38268 | beb86b805590 |
--- a/src/Pure/General/xml.scala Tue Aug 10 22:26:23 2010 +0200 +++ b/src/Pure/General/xml.scala Tue Aug 10 23:03:48 2010 +0200 @@ -30,6 +30,8 @@ def elem(name: String, body: List[Tree]) = Elem(Markup(name, Nil), body) def elem(name: String) = Elem(Markup(name, Nil), Nil) + type Body = List[Tree] + /* string representation */