Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
chaned '+'
authorimmler@in.tum.de
Fri, 22 May 2009 13:43:34 +0200
changeset 34561 8a70c2de32d3
parent 34560 08f0d81c6833
child 34562 cdf914c78ff2
chaned '+'
src/Tools/jEdit/src/prover/MarkupNode.scala file | annotate | diff | comparison | revisions 
--- 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 {
isabelle