Markup_Tree.+: new info tends to sink to bottom, where it is prefered by select;

--- a/src/Pure/PIDE/markup_tree.scala	Tue Aug 24 21:22:01 2010 +0200
+++ b/src/Pure/PIDE/markup_tree.scala	Tue Aug 24 21:34:38 2010 +0200
@@ -64,10 +64,7 @@
         new Markup_Tree(Branches.update(branches, new_info -> empty))
       case Some((info, subtree)) =>
         val range = info.range
-        if (range == new_range)  // FIXME append, not cons (!??)
-          new Markup_Tree(Branches.update(branches,
-            new_info -> new Markup_Tree(Branches.single((info, subtree)))))
-        else if (range.contains(new_range))
+        if (range.contains(new_range))
           new Markup_Tree(Branches.update(branches, info -> (subtree + new_info)))
         else if (new_range.contains(branches.head._1) && new_range.contains(branches.last._1))
           new Markup_Tree(Branches.single(new_info -> this))