# HG changeset patch
# User wenzelm
# Date 1477218431 -7200
# Node ID d9c7a8e83c3d917b2a17d57dce6f5ed97539b921
# Parent  8f628de5108bb6c14b7cdc2adbb90d14d0695859
tuned;

diff -r 8f628de5108b -r d9c7a8e83c3d src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Sun Oct 23 12:21:17 2016 +0200
+++ b/src/Pure/PIDE/xml.scala	Sun Oct 23 12:27:11 2016 +0200
@@ -22,16 +22,15 @@
   type Attributes = Properties.T
 
   sealed abstract class Tree { override def toString: String = string_of_tree(this) }
-  case class Elem(markup: Markup, body: List[Tree]) extends Tree
+  type Body = List[Tree]
+  case class Elem(markup: Markup, body: Body) extends Tree
   {
     def name: String = markup.name
   }
   case class Text(content: String) extends Tree
 
-  def elem(name: String, body: List[Tree]) = XML.Elem(Markup(name, Nil), body)
-  def elem(name: String) = XML.Elem(Markup(name, Nil), Nil)
-
-  type Body = List[Tree]
+  def elem(name: String, body: Body): XML.Elem = XML.Elem(Markup(name, Nil), body)
+  def elem(name: String): XML.Elem = XML.Elem(Markup(name, Nil), Nil)
 
 
   /* wrapped elements */