src/Pure/PIDE/xml.scala

--- a/src/Pure/PIDE/xml.scala	Fri Sep 28 17:06:07 2012 +0200
+++ b/src/Pure/PIDE/xml.scala	Fri Sep 28 22:53:18 2012 +0200
@@ -30,7 +30,59 @@
   type Body = List[Tree]
 
 
-  /* string representation */
+  /* wrapped elements */
+
+  val XML_ELEM = "xml_elem";
+  val XML_NAME = "xml_name";
+  val XML_BODY = "xml_body";
+
+  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)
+
+    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) =>
+          Some(Markup(name, props), body1, body2)
+        case _ => None
+      }
+  }
+
+
+  /* traverse text */
+
+  def traverse_text[A](body: Body)(a: A)(op: (A, String) => A): A =
+  {
+    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)
+      }
+    (a /: body)(traverse)
+  }
+
+  def text_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + s.length }
+
+
+  /* text content */
+
+  def content(body: Body): String =
+  {
+    val text = new StringBuilder(text_length(body))
+    traverse_text(body)(()) { case (_, s) => text.append(s) }
+    text.toString
+  }
+
+  def content(tree: Tree): String = content(List(tree))
+
+
+
+  /** string representation **/
 
   def string_of_body(body: Body): String =
   {
@@ -68,33 +120,6 @@
   def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
 
 
-  /* traverse text */
-
-  def traverse_text[A](body: Body)(a: A)(op: (A, String) => A): A =
-  {
-    def traverse(x: A, t: Tree): A =
-      t match {
-        case Elem(_, ts) => (x /: ts)(traverse)
-        case Text(s) => op(x, s)
-      }
-    (a /: body)(traverse)
-  }
-
-  def text_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + s.length }
-
-
-  /* text content */
-
-  def content(body: Body): String =
-  {
-    val text = new StringBuilder(text_length(body))
-    traverse_text(body)(()) { case (_, s) => text.append(s) }
-    text.toString
-  }
-
-  def content(tree: Tree): String = content(List(tree))
-
-
 
   /** cache for partial sharing (weak table) **/