src/Pure/PIDE/markup_tree.scala

--- a/src/Pure/PIDE/markup_tree.scala	Wed Mar 26 21:01:09 2014 +0100
+++ b/src/Pure/PIDE/markup_tree.scala	Thu Mar 27 10:43:43 2014 +0100
@@ -20,6 +20,9 @@
 
   val empty: Markup_Tree = new Markup_Tree(Branches.empty)
 
+  def merge(trees: List[Markup_Tree]): Markup_Tree =
+    (empty /: trees)(_ ++ _)
+
   def merge_disjoint(trees: List[Markup_Tree]): Markup_Tree =
     trees match {
       case Nil => empty
@@ -157,8 +160,12 @@
   }
 
   def ++ (other: Markup_Tree): Markup_Tree =
-    (this /: other.branches)({ case (tree, (range, entry)) =>
-      ((tree ++ entry.subtree) /: entry.markup)({ case (t, elem) => t + Text.Info(range, elem) }) })
+    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, filter: XML.Elem => Boolean): XML.Body =
   {