author | wenzelm |
Sun, 11 Mar 2018 15:05:43 +0100 | |
changeset 67818 | 2457bea123e4 |
parent 67817 | 93faefc25fe7 |
child 67819 | b73d8ed73b35 |
--- 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 */