1.1 --- a/src/Tools/jEdit/src/prover/MarkupNode.scala	Fri May 22 13:43:34 2009 +0200
     1.2 +++ b/src/Tools/jEdit/src/prover/MarkupNode.scala	Fri May 22 13:43:34 2009 +0200
     1.3 @@ -102,11 +102,12 @@
     1.4  
     1.5    def +(new_child : MarkupNode) : MarkupNode = {
     1.6      if (new_child fitting_into this) {
     1.7 -      val new_children = children.map(c => if((new_child fitting_into c)) c + new_child else c)
     1.8 -      if (new_children == children) {
     1.9 +      var inserted = false
    1.10 +      val new_children = children.map(c => if((new_child fitting_into c) && !inserted) {inserted = true; c + new_child} else c)
    1.11 +      if (!inserted) {
    1.12          // new_child did not fit into children of this -> insert new_child between this and its children
    1.13 -        val (fitting, nonfitting) = children span(_ fitting_into new_child)
    1.14 -        this remove fitting add ((new_child /: fitting) (_ add _))
    1.15 +        val fitting = children filter(_ fitting_into new_child)
    1.16 +        (this remove fitting) add ((new_child /: fitting) (_ + _))
    1.17        }
    1.18        else this set_children new_children
    1.19      } else {