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