src/Pure/PIDE/markup_tree.scala

--- a/src/Pure/PIDE/markup_tree.scala	Thu Mar 27 11:19:31 2014 +0100
+++ b/src/Pure/PIDE/markup_tree.scala	Thu Mar 27 12:11:32 2014 +0100
@@ -20,8 +20,8 @@
 
   val empty: Markup_Tree = new Markup_Tree(Branches.empty)
 
-  def merge(trees: List[Markup_Tree]): Markup_Tree =
-    (empty /: trees)(_ ++ _)
+  def merge(trees: List[Markup_Tree], range: Text.Range, elements: Document.Elements): Markup_Tree =
+    (empty /: trees)(_.merge(_, range, elements))
 
   def merge_disjoint(trees: List[Markup_Tree]): Markup_Tree =
     trees match {
@@ -116,12 +116,6 @@
   private def this(branches: Markup_Tree.Branches.T, entry: Markup_Tree.Entry) =
     this(branches + (entry.range -> entry))
 
-  override def toString =
-    branches.toList.map(_._2) match {
-      case Nil => "Empty"
-      case list => list.mkString("Tree(", ",", ")")
-    }
-
   private def overlapping(range: Text.Range): Branches.T =
   {
     val start = Text.Range(range.start)
@@ -159,43 +153,22 @@
     }
   }
 
-  def ++ (other: Markup_Tree): Markup_Tree =
-    if (this eq other) this
-    else if (branches.isEmpty) other
-    else
-      (this /: other.branches)({ case (tree, (range, entry)) =>
-        ((tree ++ entry.subtree) /: entry.markup)(
-          { case (t, elem) => t + Text.Info(range, elem) }) })
-
-  def to_XML(root_range: Text.Range, text: CharSequence, elements: Document.Elements): XML.Body =
+  def merge(other: Markup_Tree, root_range: Text.Range, elements: Document.Elements): Markup_Tree =
   {
-    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 merge_trees(tree1: Markup_Tree, tree2: Markup_Tree): Markup_Tree =
+      if (tree1 eq tree2) tree1
+      else if (tree1.branches.isEmpty) tree2
+      else
+        (tree1 /: tree2.branches)(
+          { case (tree, (range, entry)) =>
+              if (range overlaps root_range) {
+                (merge_trees(tree, entry.subtree) /: entry.filter_markup(elements))(
+                  { case (t, elem) => t + Text.Info(range, elem) })
+              }
+              else tree
+          })
 
-    def make_elems(rev_markups: List[XML.Elem], body: XML.Body): XML.Body =
-      (body /: rev_markups) {
-        case (b, elem) =>
-          if (!elements(elem.name)) b
-          else if (elem.body.isEmpty) List(XML.Elem(elem.markup, b))
-          else List(XML.Wrapped_Elem(elem.markup, elem.body, 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))
+    merge_trees(this, other)
   }
 
   def cumulate[A](root_range: Text.Range, root_info: A, elements: Document.Elements,
@@ -246,5 +219,42 @@
     traverse(root_range.start,
       List((Text.Info(root_range, root_info), overlapping(root_range).toList)))
   }
+
+  def to_XML(root_range: Text.Range, text: CharSequence, elements: Document.Elements): 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) =>
+          if (!elements(elem.name)) b
+          else if (elem.body.isEmpty) List(XML.Elem(elem.markup, b))
+          else List(XML.Wrapped_Elem(elem.markup, elem.body, 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))
+  }
+
+  override def toString =
+    branches.toList.map(_._2) match {
+      case Nil => "Empty"
+      case list => list.mkString("Tree(", ",", ")")
+    }
 }