convenience to represent XML.Body as single XML.Elem;
authorwenzelm
Sun, 11 Mar 2018 15:05:43 +0100
changeset 67818 2457bea123e4
parent 67817 93faefc25fe7
child 67819 b73d8ed73b35
convenience to represent XML.Body as single XML.Elem;
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 */