src/Pure/PIDE/markup_tree.scala
changeset 38576 ce3eed2b16f7
parent 38571 f7d7b8054648
child 38577 4e4d3ea3725a
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Sun Aug 22 16:37:15 2010 +0200
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Sun Aug 22 16:43:20 2010 +0200
     1.3 @@ -88,33 +88,6 @@
     1.4      }
     1.5    }
     1.6  
     1.7 -  // FIXME depth-first with result markup stack
     1.8 -  // FIXME projection to given range
     1.9 -  def flatten(parent: Node[Any]): List[Node[Any]] =
    1.10 -  {
    1.11 -    val result = new mutable.ListBuffer[Node[Any]]
    1.12 -    var offset = parent.range.start
    1.13 -    for ((_, (node, subtree)) <- branches.iterator) {
    1.14 -      if (offset < node.range.start)
    1.15 -        result += new Node(Text.Range(offset, node.range.start), parent.info)
    1.16 -      result ++= subtree.flatten(node)
    1.17 -      offset = node.range.stop
    1.18 -    }
    1.19 -    if (offset < parent.range.stop)
    1.20 -      result += new Node(Text.Range(offset, parent.range.stop), parent.info)
    1.21 -    result.toList
    1.22 -  }
    1.23 -
    1.24 -  def filter(pred: Node[Any] => Boolean): Markup_Tree =
    1.25 -  {
    1.26 -    val bs = branches.toList.flatMap(entry => {
    1.27 -      val (_, (node, subtree)) = entry
    1.28 -      if (pred(node)) List((node, (node, subtree.filter(pred))))
    1.29 -      else subtree.filter(pred).branches.toList
    1.30 -    })
    1.31 -    new Markup_Tree(Branches.empty ++ bs)
    1.32 -  }
    1.33 -
    1.34    def select[A](root: Node[A])(sel: PartialFunction[Any, A]): Stream[Node[A]] =
    1.35    {
    1.36      def stream(parent: Node[A], bs: Branches.T): Stream[Node[A]] =