src/Pure/PIDE/markup_node.scala

 import javax.swing.tree.DefaultMutableTreeNode
 
 
 
 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])
 {
   private def add(branch: Markup_Tree) =   // FIXME avoid sort
     copy(branches = (branch :: branches).sortWith((a, b) => a.node.range.start < b.node.range.start))

     copy(branches = branches.filterNot(bs.contains(_)))
 
   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
           }
           else branch)
       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)
     }
     else {

       else branches
     }
     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 =
   {
     def swing(tree: Markup_Tree): DefaultMutableTreeNode =
     {