# HG changeset patch
# User wenzelm
# Date 1282133053 -7200
# Node ID 7766812a01e775737b8d38b4d7a97a720f33c89b
# Parent  f01f4ab2a0af6ff925cb3b8c3ad98860a8f8bd8c
tuned;

diff -r f01f4ab2a0af -r 7766812a01e7 src/Pure/PIDE/markup_node.scala
--- a/src/Pure/PIDE/markup_node.scala	Wed Aug 18 14:02:32 2010 +0200
+++ b/src/Pure/PIDE/markup_node.scala	Wed Aug 18 14:04:13 2010 +0200
@@ -13,11 +13,6 @@
 
 
 case class Markup_Node(val range: Text.Range, val info: Any)
-{
-  def fits_into(that: Markup_Node): Boolean =
-    that.range.start <= this.range.start && this.range.stop <= that.range.stop
-}
-
 
 case class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree])
 {
@@ -30,11 +25,11 @@
   def + (new_tree: Markup_Tree): Markup_Tree =
   {
     val new_node = new_tree.node
-    if (new_node fits_into node) {
+    if (node.range contains new_node.range) {
       var inserted = false
       val new_branches =
         branches.map(branch =>
-          if ((new_node fits_into branch.node) && !inserted) {
+          if ((branch.node.range contains new_node.range) && !inserted) {
             inserted = true
             branch + new_tree
           }
@@ -42,7 +37,7 @@
       if (!inserted) {
         // new_tree did not fit into children of this
         // -> insert between this and its branches
-        val fitting = branches filter(_.node fits_into new_node)
+        val fitting = branches filter(new_node.range contains _.node.range)
         (this remove fitting) add ((new_tree /: fitting)(_ + _))
       }
       else copy(branches = new_branches)
@@ -94,7 +89,7 @@
     new Markup_Text(markup.flatMap(filt(_)), content)
   }
 
-  def flatten: List[Markup_Node] = markup.flatten(_.flatten)
+  def flatten: List[Markup_Node] = markup.flatMap(_.flatten)
 
   def swing_tree(swing_node: Markup_Node => DefaultMutableTreeNode): DefaultMutableTreeNode =
   {