# HG changeset patch
# User wenzelm
# Date 1520777143 -3600
# Node ID 2457bea123e4f0d54880110ffcc3bc4fb4ffbcda
# Parent  93faefc25fe70cf7cef66cdecdf9957b76be8764
convenience to represent XML.Body as single XML.Elem;

diff -r 93faefc25fe7 -r 2457bea123e4 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 */