# HG changeset patch
# User immler@in.tum.de
# Date 1242992614 -7200
# Node ID 8a70c2de32d313662df659e0da07a4bdf8c23184
# Parent  08f0d81c6833371b25a6f24910afa115f0fcbefe
chaned '+'

diff -r 08f0d81c6833 -r 8a70c2de32d3 src/Tools/jEdit/src/prover/MarkupNode.scala
--- a/src/Tools/jEdit/src/prover/MarkupNode.scala	Fri May 22 13:43:34 2009 +0200
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala	Fri May 22 13:43:34 2009 +0200
@@ -102,11 +102,12 @@
 
   def +(new_child : MarkupNode) : MarkupNode = {
     if (new_child fitting_into this) {
-      val new_children = children.map(c => if((new_child fitting_into c)) c + new_child else c)
-      if (new_children == children) {
+      var inserted = false
+      val new_children = children.map(c => if((new_child fitting_into c) && !inserted) {inserted = true; c + new_child} else c)
+      if (!inserted) {
         // new_child did not fit into children of this -> insert new_child between this and its children
-        val (fitting, nonfitting) = children span(_ fitting_into new_child)
-        this remove fitting add ((new_child /: fitting) (_ add _))
+        val fitting = children filter(_ fitting_into new_child)
+        (this remove fitting) add ((new_child /: fitting) (_ + _))
       }
       else this set_children new_children
     } else {