# HG changeset patch
# User wenzelm
# Date 1395921640 -3600
# Node ID c63ab52630086d9d118c3abd0e2bd3348fb2e200
# Parent  1da7b4c33db970443ce6eae32e0a06d70b1d64f8
more frugal merge of markup trees: non-overlapping tree counts as empty;

diff -r 1da7b4c33db9 -r c63ab5263008 src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Thu Mar 27 12:11:32 2014 +0100
+++ b/src/Pure/PIDE/markup_tree.scala	Thu Mar 27 13:00:40 2014 +0100
@@ -116,6 +116,10 @@
   private def this(branches: Markup_Tree.Branches.T, entry: Markup_Tree.Entry) =
     this(branches + (entry.range -> entry))
 
+  def overlaps(range: Text.Range): Boolean =
+    !branches.isEmpty &&
+    Text.Range(branches.firstKey.start, branches.lastKey.stop).overlaps(range)
+
   private def overlapping(range: Text.Range): Branches.T =
   {
     val start = Text.Range(range.start)
@@ -156,19 +160,18 @@
   def merge(other: Markup_Tree, root_range: Text.Range, elements: Document.Elements): Markup_Tree =
   {
     def merge_trees(tree1: Markup_Tree, tree2: Markup_Tree): Markup_Tree =
-      if (tree1 eq tree2) tree1
-      else if (tree1.branches.isEmpty) tree2
+      if (tree1.eq(tree2) || !tree2.overlaps(root_range)) tree1
       else
         (tree1 /: tree2.branches)(
           { case (tree, (range, entry)) =>
-              if (range overlaps root_range) {
+              if (!range.overlaps(root_range)) tree
+              else
                 (merge_trees(tree, entry.subtree) /: entry.filter_markup(elements))(
                   { case (t, elem) => t + Text.Info(range, elem) })
-              }
-              else tree
           })
 
-    merge_trees(this, other)
+    if (!this.overlaps(root_range)) other
+    else merge_trees(this, other)
   }
 
   def cumulate[A](root_range: Text.Range, root_info: A, elements: Document.Elements,