# HG changeset patch
# User wenzelm
# Date 1282488200 -7200
# Node ID ce3eed2b16f77da6b07ebe275473f73e7b6c39a6
# Parent  80d962964216773961521fc4913593d291e09f29
removed obsolete Markup_Tree.flatten/filter;

diff -r 80d962964216 -r ce3eed2b16f7 src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Sun Aug 22 16:37:15 2010 +0200
+++ b/src/Pure/PIDE/markup_tree.scala	Sun Aug 22 16:43:20 2010 +0200
@@ -88,33 +88,6 @@
     }
   }
 
-  // FIXME depth-first with result markup stack
-  // FIXME projection to given range
-  def flatten(parent: Node[Any]): List[Node[Any]] =
-  {
-    val result = new mutable.ListBuffer[Node[Any]]
-    var offset = parent.range.start
-    for ((_, (node, subtree)) <- branches.iterator) {
-      if (offset < node.range.start)
-        result += new Node(Text.Range(offset, node.range.start), parent.info)
-      result ++= subtree.flatten(node)
-      offset = node.range.stop
-    }
-    if (offset < parent.range.stop)
-      result += new Node(Text.Range(offset, parent.range.stop), parent.info)
-    result.toList
-  }
-
-  def filter(pred: Node[Any] => Boolean): Markup_Tree =
-  {
-    val bs = branches.toList.flatMap(entry => {
-      val (_, (node, subtree)) = entry
-      if (pred(node)) List((node, (node, subtree.filter(pred))))
-      else subtree.filter(pred).branches.toList
-    })
-    new Markup_Tree(Branches.empty ++ bs)
-  }
-
   def select[A](root: Node[A])(sel: PartialFunction[Any, A]): Stream[Node[A]] =
   {
     def stream(parent: Node[A], bs: Branches.T): Stream[Node[A]] =