# HG changeset patch # User wenzelm # Date 1348140867 -7200 # Node ID 25b7e843e124a55312d347aa9f62df6fb566dcfe # Parent 99ed1f422635a6d8f9693e8354cf03cfae0a2888 more direct Markup_Tree.from_XML; diff -r 99ed1f422635 -r 25b7e843e124 src/Pure/PIDE/markup_tree.scala --- a/src/Pure/PIDE/markup_tree.scala Thu Sep 20 11:09:53 2012 +0200 +++ b/src/Pure/PIDE/markup_tree.scala Thu Sep 20 13:34:27 2012 +0200 @@ -12,12 +12,28 @@ import javax.swing.tree.DefaultMutableTreeNode import scala.collection.immutable.SortedMap +import scala.annotation.tailrec object Markup_Tree { val empty: Markup_Tree = new Markup_Tree(Branches.empty) + def merge_disjoint(trees: List[Markup_Tree]): Markup_Tree = + trees match { + case Nil => empty + case head :: tail => + new Markup_Tree( + (head.branches /: tail) { + case (branches, tree) => + (branches /: tree.branches) { + case (bs, (r, entry)) => + require(!bs.isDefinedAt(r)) + bs + (r -> entry) + } + }) + } + object Entry { def apply(markup: Text.Markup, subtree: Markup_Tree): Entry = @@ -35,53 +51,55 @@ else copy(rev_markup = info :: rev_markup, elements = elements + info.markup.name) def markup: List[XML.Elem] = rev_markup.reverse - - def reverse_markup: Entry = - copy(rev_markup = rev_markup.reverse, subtree = subtree.reverse_markup) } object Branches { type T = SortedMap[Text.Range, Entry] val empty: T = SortedMap.empty(Text.Range.Ordering) - - def reverse_markup(branches: T): T = - (empty /: branches.iterator) { case (bs, (r, entry)) => bs + (r -> entry.reverse_markup) } } /* XML representation */ - def from_XML(body: XML.Body): Markup_Tree = - { - var offset = 0 - var markup_tree = empty + @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) + case _ => (markups, body) + } + + private def make_trees(acc: (Int, List[Markup_Tree]), tree: XML.Tree): (Int, List[Markup_Tree]) = + { + val (offset, markup_trees) = acc + + strip_elems(Nil, List(tree)) match { + case (Nil, body) => + (offset + XML.text_length(body), markup_trees) - def traverse(tree: XML.Tree): Unit = - tree match { - case XML.Elem(markup, trees) => - val start = offset - trees.foreach(traverse) - val stop = offset - markup_tree += Text.Info(Text.Range(start, stop), XML.Elem(markup, Nil)) - case XML.Text(s) => offset += s.length + case (markups, body) => + val (end_offset, markup_trees1) = (acc /: body)(make_trees) + val range = Text.Range(offset, end_offset) + val new_markup_tree = + (merge_disjoint(markup_trees1) /: markups) { + case (markup_tree, markup) => + markup_tree + Text.Info(range, XML.Elem(markup, Nil)) + } + (end_offset, List(new_markup_tree)) } - body.foreach(traverse) + } - markup_tree.reverse_markup - } + def from_XML(body: XML.Body): Markup_Tree = + merge_disjoint(((0, Nil: List[Markup_Tree]) /: body)(make_trees)._2) } -final class Markup_Tree private(branches: Markup_Tree.Branches.T) +final class Markup_Tree private(private val branches: Markup_Tree.Branches.T) { import Markup_Tree._ private def this(branches: Markup_Tree.Branches.T, entry: Markup_Tree.Entry) = this(branches + (entry.range -> entry)) - def reverse_markup: Markup_Tree = new Markup_Tree(Branches.reverse_markup(branches)) - override def toString = branches.toList.map(_._2) match { case Nil => "Empty"