more direct Markup_Tree.from_XML;
authorwenzelm
Thu Sep 20 13:34:27 2012 +0200 (2012-09-20)
changeset 4946725b7e843e124
parent 49466 99ed1f422635
child 49468 8b06b99fb85c
more direct Markup_Tree.from_XML;
src/Pure/PIDE/markup_tree.scala
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Thu Sep 20 11:09:53 2012 +0200
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Thu Sep 20 13:34:27 2012 +0200
     1.3 @@ -12,12 +12,28 @@
     1.4  import javax.swing.tree.DefaultMutableTreeNode
     1.5  
     1.6  import scala.collection.immutable.SortedMap
     1.7 +import scala.annotation.tailrec
     1.8  
     1.9  
    1.10  object Markup_Tree
    1.11  {
    1.12    val empty: Markup_Tree = new Markup_Tree(Branches.empty)
    1.13  
    1.14 +  def merge_disjoint(trees: List[Markup_Tree]): Markup_Tree =
    1.15 +    trees match {
    1.16 +      case Nil => empty
    1.17 +      case head :: tail =>
    1.18 +        new Markup_Tree(
    1.19 +          (head.branches /: tail) {
    1.20 +            case (branches, tree) =>
    1.21 +              (branches /: tree.branches) {
    1.22 +                case (bs, (r, entry)) =>
    1.23 +                  require(!bs.isDefinedAt(r))
    1.24 +                  bs + (r -> entry)
    1.25 +              }
    1.26 +          })
    1.27 +    }
    1.28 +
    1.29    object Entry
    1.30    {
    1.31      def apply(markup: Text.Markup, subtree: Markup_Tree): Entry =
    1.32 @@ -35,53 +51,55 @@
    1.33        else copy(rev_markup = info :: rev_markup, elements = elements + info.markup.name)
    1.34  
    1.35      def markup: List[XML.Elem] = rev_markup.reverse
    1.36 -
    1.37 -    def reverse_markup: Entry =
    1.38 -      copy(rev_markup = rev_markup.reverse, subtree = subtree.reverse_markup)
    1.39    }
    1.40  
    1.41    object Branches
    1.42    {
    1.43      type T = SortedMap[Text.Range, Entry]
    1.44      val empty: T = SortedMap.empty(Text.Range.Ordering)
    1.45 -
    1.46 -    def reverse_markup(branches: T): T =
    1.47 -      (empty /: branches.iterator) { case (bs, (r, entry)) => bs + (r -> entry.reverse_markup) }
    1.48    }
    1.49  
    1.50  
    1.51    /* XML representation */
    1.52  
    1.53 -  def from_XML(body: XML.Body): Markup_Tree =
    1.54 -  {
    1.55 -    var offset = 0
    1.56 -    var markup_tree = empty
    1.57 +  @tailrec private def strip_elems(markups: List[Markup], body: XML.Body): (List[Markup], XML.Body) =
    1.58 +    body match {
    1.59 +      case List(XML.Elem(markup1, body1)) => strip_elems(markup1 :: markups, body1)
    1.60 +      case _ => (markups, body)
    1.61 +    }
    1.62 +
    1.63 +  private def make_trees(acc: (Int, List[Markup_Tree]), tree: XML.Tree): (Int, List[Markup_Tree]) =
    1.64 +    {
    1.65 +      val (offset, markup_trees) = acc
    1.66 +
    1.67 +      strip_elems(Nil, List(tree)) match {
    1.68 +        case (Nil, body) =>
    1.69 +          (offset + XML.text_length(body), markup_trees)
    1.70  
    1.71 -    def traverse(tree: XML.Tree): Unit =
    1.72 -      tree match {
    1.73 -        case XML.Elem(markup, trees) =>
    1.74 -          val start = offset
    1.75 -          trees.foreach(traverse)
    1.76 -          val stop = offset
    1.77 -          markup_tree += Text.Info(Text.Range(start, stop), XML.Elem(markup, Nil))
    1.78 -        case XML.Text(s) => offset += s.length
    1.79 +        case (markups, body) =>
    1.80 +          val (end_offset, markup_trees1) = (acc /: body)(make_trees)
    1.81 +          val range = Text.Range(offset, end_offset)
    1.82 +          val new_markup_tree =
    1.83 +            (merge_disjoint(markup_trees1) /: markups) {
    1.84 +              case (markup_tree, markup) =>
    1.85 +                markup_tree + Text.Info(range, XML.Elem(markup, Nil))
    1.86 +            }
    1.87 +          (end_offset, List(new_markup_tree))
    1.88        }
    1.89 -    body.foreach(traverse)
    1.90 +    }
    1.91  
    1.92 -    markup_tree.reverse_markup
    1.93 -  }
    1.94 +  def from_XML(body: XML.Body): Markup_Tree =
    1.95 +    merge_disjoint(((0, Nil: List[Markup_Tree]) /: body)(make_trees)._2)
    1.96  }
    1.97  
    1.98  
    1.99 -final class Markup_Tree private(branches: Markup_Tree.Branches.T)
   1.100 +final class Markup_Tree private(private val branches: Markup_Tree.Branches.T)
   1.101  {
   1.102    import Markup_Tree._
   1.103  
   1.104    private def this(branches: Markup_Tree.Branches.T, entry: Markup_Tree.Entry) =
   1.105      this(branches + (entry.range -> entry))
   1.106  
   1.107 -  def reverse_markup: Markup_Tree = new Markup_Tree(Branches.reverse_markup(branches))
   1.108 -
   1.109    override def toString =
   1.110      branches.toList.map(_._2) match {
   1.111        case Nil => "Empty"