# HG changeset patch
# User wenzelm
# Date 1440591211 -7200
# Node ID 397354b299351ef305e6b2534aafa695b2b19348
# Parent  636b578bfaddd9fd09c904b1c3d820cba1f4236d
tuned signature;

diff -r 636b578bfadd -r 397354b29935 src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Wed Aug 26 13:43:24 2015 +0200
+++ b/src/Pure/PIDE/xml.scala	Wed Aug 26 14:13:31 2015 +0200
@@ -28,8 +28,8 @@
   }
   case class Text(content: String) extends Tree
 
-  def elem(name: String, body: List[Tree]) = Elem(Markup(name, Nil), body)
-  def elem(name: String) = Elem(Markup(name, Nil), Nil)
+  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]
 
@@ -43,14 +43,14 @@
   object Wrapped_Elem
   {
     def apply(markup: Markup, body1: Body, body2: Body): XML.Elem =
-      Elem(Markup(XML_ELEM, (XML_NAME, markup.name) :: markup.properties),
-        Elem(Markup(XML_BODY, Nil), body1) :: body2)
+      XML.Elem(Markup(XML_ELEM, (XML_NAME, markup.name) :: markup.properties),
+        XML.Elem(Markup(XML_BODY, Nil), body1) :: body2)
 
     def unapply(tree: Tree): Option[(Markup, Body, Body)] =
       tree match {
         case
-          Elem(Markup(XML_ELEM, (XML_NAME, name) :: props),
-            Elem(Markup(XML_BODY, Nil), body1) :: body2) =>
+          XML.Elem(Markup(XML_ELEM, (XML_NAME, name) :: props),
+            XML.Elem(Markup(XML_BODY, Nil), body1) :: body2) =>
           Some(Markup(name, props), body1, body2)
         case _ => None
       }
@@ -63,9 +63,9 @@
   {
     def traverse(x: A, t: Tree): A =
       t match {
-        case Wrapped_Elem(_, _, ts) => (x /: ts)(traverse)
-        case Elem(_, ts) => (x /: ts)(traverse)
-        case Text(s) => op(x, s)
+        case XML.Wrapped_Elem(_, _, ts) => (x /: ts)(traverse)
+        case XML.Elem(_, ts) => (x /: ts)(traverse)
+        case XML.Text(s) => op(x, s)
       }
     (a /: body)(traverse)
   }
@@ -109,13 +109,13 @@
     def elem(markup: Markup) { s ++= markup.name; markup.properties.foreach(attrib) }
     def tree(t: Tree): Unit =
       t match {
-        case Elem(markup, Nil) =>
+        case XML.Elem(markup, Nil) =>
           s ++= "<"; elem(markup); s ++= "/>"
-        case Elem(markup, ts) =>
+        case XML.Elem(markup, ts) =>
           s ++= "<"; elem(markup); s ++= ">"
           ts.foreach(tree)
           s ++= "</"; s ++= markup.name; s ++= ">"
-        case Text(txt) => text(txt)
+        case XML.Text(txt) => text(txt)
       }
     body.foreach(tree)
     s.toString