Markup_Tree.+: new info tends to sink to bottom, where it is prefered by select;
authorwenzelm
Tue Aug 24 21:34:38 2010 +0200 (2010-08-24)
changeset 38661f1ba2ae8e58a
parent 38660 049fdf15144f
child 38662 4d4553e09337
Markup_Tree.+: new info tends to sink to bottom, where it is prefered by select;
src/Pure/PIDE/markup_tree.scala
     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))