src/Pure/PIDE/markup_tree.scala
changeset 45468 33e946d3f449
parent 45467 3f290b6288cf
child 45469 25306d92f4ad
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Sat Nov 12 11:45:49 2011 +0100
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Sat Nov 12 12:21:42 2011 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4  object Markup_Tree
     1.5  {
     1.6    sealed case class Cumulate[A](info: A, result: PartialFunction[(A, Text.Markup), A])
     1.7 -  type Select[A] = PartialFunction[Text.Markup, A]
     1.8 +  sealed case class Select[A](result: PartialFunction[Text.Markup, A])
     1.9  
    1.10    val empty: Markup_Tree = new Markup_Tree(Branches.empty)
    1.11  
    1.12 @@ -124,43 +124,6 @@
    1.13        List((Text.Info(root_range, root_info), overlapping(root_range).toStream)))
    1.14    }
    1.15  
    1.16 -  def select[A](root_range: Text.Range)(result: Select[A]): Stream[Text.Info[Option[A]]] =
    1.17 -  {
    1.18 -    def stream(
    1.19 -      last: Text.Offset,
    1.20 -      stack: List[(Text.Info[Option[A]], Stream[(Text.Range, Branches.Entry)])])
    1.21 -        : Stream[Text.Info[Option[A]]] =
    1.22 -    {
    1.23 -      stack match {
    1.24 -        case (parent, (range, (info, tree)) #:: more) :: rest =>
    1.25 -          val subrange = range.restrict(root_range)
    1.26 -          val subtree = tree.overlapping(subrange).toStream
    1.27 -          val start = subrange.start
    1.28 -
    1.29 -          if (result.isDefinedAt(info)) {
    1.30 -            val next = Text.Info[Option[A]](subrange, Some(result(info)))
    1.31 -            val nexts = stream(start, (next, subtree) :: (parent, more) :: rest)
    1.32 -            if (last < start) parent.restrict(Text.Range(last, start)) #:: nexts
    1.33 -            else nexts
    1.34 -          }
    1.35 -          else stream(last, (parent, subtree #::: more) :: rest)
    1.36 -
    1.37 -        case (parent, Stream.Empty) :: rest =>
    1.38 -          val stop = parent.range.stop
    1.39 -          val nexts = stream(stop, rest)
    1.40 -          if (last < stop) parent.restrict(Text.Range(last, stop)) #:: nexts
    1.41 -          else nexts
    1.42 -
    1.43 -        case Nil =>
    1.44 -          val stop = root_range.stop
    1.45 -          if (last < stop) Stream(Text.Info(Text.Range(last, stop), None))
    1.46 -          else Stream.empty
    1.47 -      }
    1.48 -    }
    1.49 -    stream(root_range.start,
    1.50 -      List((Text.Info(root_range, None), overlapping(root_range).toStream)))
    1.51 -  }
    1.52 -
    1.53    def swing_tree(parent: DefaultMutableTreeNode)
    1.54      (swing_node: Text.Markup => DefaultMutableTreeNode)
    1.55    {