src/Pure/PIDE/markup_tree.scala

           }
         }
     }
   }
 
+  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) }) })
+
   def to_XML(root_range: Text.Range, text: CharSequence, filter: XML.Elem => Boolean): 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))