src/Pure/PIDE/xml.scala

--- a/src/Pure/PIDE/xml.scala	Sun Mar 11 13:18:41 2018 +0100
+++ b/src/Pure/PIDE/xml.scala	Sun Mar 11 15:05:43 2018 +0100
@@ -62,6 +62,16 @@
       }
   }
 
+  object Root_Elem
+  {
+    def apply(body: Body): XML.Elem = XML.Elem(Markup(XML_ELEM, Nil), body)
+    def unapply(tree: Tree): Option[Body] =
+      tree match {
+        case XML.Elem(Markup(XML_ELEM, Nil), body) => Some(body)
+        case _ => None
+      }
+  }
+
 
   /* traverse text */