1.1 --- a/src/Pure/PIDE/markup_tree.scala	Thu Mar 27 12:11:32 2014 +0100
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Thu Mar 27 13:00:40 2014 +0100
     1.3 @@ -116,6 +116,10 @@
     1.4    private def this(branches: Markup_Tree.Branches.T, entry: Markup_Tree.Entry) =
     1.5      this(branches + (entry.range -> entry))
     1.6  
     1.7 +  def overlaps(range: Text.Range): Boolean =
     1.8 +    !branches.isEmpty &&
     1.9 +    Text.Range(branches.firstKey.start, branches.lastKey.stop).overlaps(range)
    1.10 +
    1.11    private def overlapping(range: Text.Range): Branches.T =
    1.12    {
    1.13      val start = Text.Range(range.start)
    1.14 @@ -156,19 +160,18 @@
    1.15    def merge(other: Markup_Tree, root_range: Text.Range, elements: Document.Elements): Markup_Tree =
    1.16    {
    1.17      def merge_trees(tree1: Markup_Tree, tree2: Markup_Tree): Markup_Tree =
    1.18 -      if (tree1 eq tree2) tree1
    1.19 -      else if (tree1.branches.isEmpty) tree2
    1.20 +      if (tree1.eq(tree2) || !tree2.overlaps(root_range)) tree1
    1.21        else
    1.22          (tree1 /: tree2.branches)(
    1.23            { case (tree, (range, entry)) =>
    1.24 -              if (range overlaps root_range) {
    1.25 +              if (!range.overlaps(root_range)) tree
    1.26 +              else
    1.27                  (merge_trees(tree, entry.subtree) /: entry.filter_markup(elements))(
    1.28                    { case (t, elem) => t + Text.Info(range, elem) })
    1.29 -              }
    1.30 -              else tree
    1.31            })
    1.32  
    1.33 -    merge_trees(this, other)
    1.34 +    if (!this.overlaps(root_range)) other
    1.35 +    else merge_trees(this, other)
    1.36    }
    1.37  
    1.38    def cumulate[A](root_range: Text.Range, root_info: A, elements: Document.Elements,