# HG changeset patch
# User wenzelm
# Date 1395948499 -3600
# Node ID 2bdf8261677a579297afde2415db680e1517c3df
# Parent  0fc032898b056e80c929d8faf90032e1524c08b7
more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);

diff -r 0fc032898b05 -r 2bdf8261677a src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Thu Mar 27 19:47:30 2014 +0100
+++ b/src/Pure/PIDE/markup_tree.scala	Thu Mar 27 20:28:19 2014 +0100
@@ -116,10 +116,6 @@
   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)
@@ -131,6 +127,11 @@
     }
   }
 
+  def restrict(range: Text.Range): Markup_Tree =
+    new Markup_Tree(overlapping(range))
+
+  def is_empty: Boolean = branches.isEmpty
+
   def + (new_markup: Text.Markup): Markup_Tree =
   {
     val new_range = new_markup.range
@@ -160,18 +161,21 @@
   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) || !tree2.overlaps(root_range)) tree1
-      else
-        (tree1 /: tree2.branches)(
-          { case (tree, (range, entry)) =>
-              if (!range.overlaps(root_range)) tree
-              else
-                (merge_trees(tree, entry.subtree) /: entry.filter_markup(elements))(
-                  { case (t, elem) => t + Text.Info(range, elem) })
-          })
+      (tree1 /: tree2.branches)(
+        { case (tree, (range, entry)) =>
+            if (!range.overlaps(root_range)) tree
+            else
+              (merge_trees(tree, entry.subtree) /: entry.filter_markup(elements))(
+                { case (t, elem) => t + Text.Info(range, elem) })
+        })
 
-    if (!this.overlaps(root_range)) other
-    else merge_trees(this, other)
+    if (this eq other) this
+    else {
+      val tree1 = this.restrict(root_range)
+      val tree2 = other.restrict(root_range)
+      if (tree1.is_empty) tree2
+      else merge_trees(tree1, tree2)
+    }
   }
 
   def cumulate[A](root_range: Text.Range, root_info: A, elements: Document.Elements,