operations to turn markup into XML;
authorwenzelm
Thu Sep 27 19:34:31 2012 +0200 (2012-09-27)
changeset 496140009a6ebc83b
parent 49613 2f6986e2ef06
child 49624 9d34cfe1dbdf
operations to turn markup into XML;
tuned;
src/Pure/PIDE/command.scala
src/Pure/PIDE/markup_tree.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Thu Sep 27 15:55:38 2012 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Thu Sep 27 19:34:31 2012 +0200
     1.3 @@ -23,6 +23,9 @@
     1.4      val results: SortedMap[Long, XML.Tree] = SortedMap.empty,
     1.5      val markup: Markup_Tree = Markup_Tree.empty)
     1.6    {
     1.7 +    def markup_to_XML: XML.Body = markup.to_XML(command.source)
     1.8 +
     1.9 +
    1.10      /* accumulate content */
    1.11  
    1.12      private def add_status(st: Markup): State = copy(status = st :: status)
     2.1 --- a/src/Pure/PIDE/markup_tree.scala	Thu Sep 27 15:55:38 2012 +0200
     2.2 +++ b/src/Pure/PIDE/markup_tree.scala	Thu Sep 27 19:34:31 2012 +0200
     2.3 @@ -12,6 +12,7 @@
     2.4  import javax.swing.tree.DefaultMutableTreeNode
     2.5  
     2.6  import scala.collection.immutable.SortedMap
     2.7 +import scala.collection.mutable
     2.8  import scala.annotation.tailrec
     2.9  
    2.10  
    2.11 @@ -65,6 +66,7 @@
    2.12  
    2.13    /* XML representation */
    2.14  
    2.15 +  // FIXME decode markup body
    2.16    @tailrec private def strip_elems(markups: List[Markup], body: XML.Body): (List[Markup], XML.Body) =
    2.17      body match {
    2.18        case List(XML.Elem(markup1, body1)) => strip_elems(markup1 :: markups, body1)
    2.19 @@ -142,13 +144,45 @@
    2.20      }
    2.21    }
    2.22  
    2.23 +  def to_XML(root_range: Text.Range, text: CharSequence, filter: XML.Elem => Boolean): XML.Body =
    2.24 +  {
    2.25 +    def make_text(start: Text.Offset, stop: Text.Offset): XML.Body =
    2.26 +      if (start == stop) Nil
    2.27 +      else List(XML.Text(text.subSequence(start, stop).toString))
    2.28 +
    2.29 +    def make_elems(rev_markups: List[XML.Elem], body: XML.Body): XML.Body =
    2.30 +      (body /: rev_markups) {
    2.31 +        case (b, elem) => // FIXME encode markup body
    2.32 +          if (filter(elem)) List(XML.Elem(elem.markup, b)) else b
    2.33 +      }
    2.34 +
    2.35 +    def make_body(elem_range: Text.Range, elem_markup: List[XML.Elem], entries: Branches.T)
    2.36 +      : XML.Body =
    2.37 +    {
    2.38 +      val body = new mutable.ListBuffer[XML.Tree]
    2.39 +      var last = elem_range.start
    2.40 +      for ((range, entry) <- entries) {
    2.41 +        val subrange = range.restrict(elem_range)
    2.42 +        body ++= make_text(last, subrange.start)
    2.43 +        body ++= make_body(subrange, entry.rev_markup, entry.subtree.overlapping(subrange))
    2.44 +        last = subrange.stop
    2.45 +      }
    2.46 +      body ++= make_text(last, elem_range.stop)
    2.47 +      make_elems(elem_markup, body.toList)
    2.48 +    }
    2.49 +   make_body(root_range, Nil, overlapping(root_range))
    2.50 +  }
    2.51 +
    2.52 +  def to_XML(text: CharSequence): XML.Body =
    2.53 +    to_XML(Text.Range(0, text.length), text, (_: XML.Elem) => true)
    2.54 +
    2.55    def cumulate[A](root_range: Text.Range, root_info: A, result_elements: Option[Set[String]],
    2.56      result: PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]] =
    2.57    {
    2.58      def results(x: A, entry: Entry): Option[A] =
    2.59        if (result_elements match { case Some(es) => es.exists(entry.elements) case None => true }) {
    2.60          val (y, changed) =
    2.61 -          (entry.markup :\ (x, false))((info, res) =>
    2.62 +          ((x, false) /: entry.rev_markup)((res, info) =>  // FIXME proper order!?
    2.63              {
    2.64                val (y, changed) = res
    2.65                val arg = (y, Text.Info(entry.range, info))