# HG changeset patch
# User wenzelm
# Date 1348767271 -7200
# Node ID 0009a6ebc83bbcc84eeb2003daf36228629ba968
# Parent  2f6986e2ef06a758a7a3be263339b29b6636c8e2
operations to turn markup into XML;
tuned;

diff -r 2f6986e2ef06 -r 0009a6ebc83b src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Thu Sep 27 15:55:38 2012 +0200
+++ b/src/Pure/PIDE/command.scala	Thu Sep 27 19:34:31 2012 +0200
@@ -23,6 +23,9 @@
     val results: SortedMap[Long, XML.Tree] = SortedMap.empty,
     val markup: Markup_Tree = Markup_Tree.empty)
   {
+    def markup_to_XML: XML.Body = markup.to_XML(command.source)
+
+
     /* accumulate content */
 
     private def add_status(st: Markup): State = copy(status = st :: status)
diff -r 2f6986e2ef06 -r 0009a6ebc83b src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Thu Sep 27 15:55:38 2012 +0200
+++ b/src/Pure/PIDE/markup_tree.scala	Thu Sep 27 19:34:31 2012 +0200
@@ -12,6 +12,7 @@
 import javax.swing.tree.DefaultMutableTreeNode
 
 import scala.collection.immutable.SortedMap
+import scala.collection.mutable
 import scala.annotation.tailrec
 
 
@@ -65,6 +66,7 @@
 
   /* XML representation */
 
+  // FIXME decode markup body
   @tailrec private def strip_elems(markups: List[Markup], body: XML.Body): (List[Markup], XML.Body) =
     body match {
       case List(XML.Elem(markup1, body1)) => strip_elems(markup1 :: markups, body1)
@@ -142,13 +144,45 @@
     }
   }
 
+  def to_XML(root_range: Text.Range, text: CharSequence, filter: XML.Elem => Boolean): XML.Body =
+  {
+    def make_text(start: Text.Offset, stop: Text.Offset): XML.Body =
+      if (start == stop) Nil
+      else List(XML.Text(text.subSequence(start, stop).toString))
+
+    def make_elems(rev_markups: List[XML.Elem], body: XML.Body): XML.Body =
+      (body /: rev_markups) {
+        case (b, elem) => // FIXME encode markup body
+          if (filter(elem)) List(XML.Elem(elem.markup, b)) else b
+      }
+
+    def make_body(elem_range: Text.Range, elem_markup: List[XML.Elem], entries: Branches.T)
+      : XML.Body =
+    {
+      val body = new mutable.ListBuffer[XML.Tree]
+      var last = elem_range.start
+      for ((range, entry) <- entries) {
+        val subrange = range.restrict(elem_range)
+        body ++= make_text(last, subrange.start)
+        body ++= make_body(subrange, entry.rev_markup, entry.subtree.overlapping(subrange))
+        last = subrange.stop
+      }
+      body ++= make_text(last, elem_range.stop)
+      make_elems(elem_markup, body.toList)
+    }
+   make_body(root_range, Nil, overlapping(root_range))
+  }
+
+  def to_XML(text: CharSequence): XML.Body =
+    to_XML(Text.Range(0, text.length), text, (_: XML.Elem) => true)
+
   def cumulate[A](root_range: Text.Range, root_info: A, result_elements: Option[Set[String]],
     result: PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]] =
   {
     def results(x: A, entry: Entry): Option[A] =
       if (result_elements match { case Some(es) => es.exists(entry.elements) case None => true }) {
         val (y, changed) =
-          (entry.markup :\ (x, false))((info, res) =>
+          ((x, false) /: entry.rev_markup)((res, info) =>  // FIXME proper order!?
             {
               val (y, changed) = res
               val arg = (y, Text.Info(entry.range, info))