src/Pure/PIDE/markup_tree.scala
changeset 39178 83e9f3ccea9f
parent 39177 0468964aec11
child 43520 cec9b95fa35d
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Tue Sep 07 22:28:58 2010 +0200
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Tue Sep 07 23:06:52 2010 +0200
     1.3 @@ -43,6 +43,8 @@
     1.4    }
     1.5  
     1.6    val empty = new Markup_Tree(Branches.empty)
     1.7 +
     1.8 +  type Select[A] = PartialFunction[Text.Info[Any], A]
     1.9  }
    1.10  
    1.11  
    1.12 @@ -89,7 +91,7 @@
    1.13    private def overlapping(range: Text.Range): Stream[(Text.Range, Branches.Entry)] =
    1.14      Branches.overlapping(range, branches).toStream
    1.15  
    1.16 -  def select[A](root_range: Text.Range)(result: PartialFunction[Text.Info[Any], A])
    1.17 +  def select[A](root_range: Text.Range)(result: Markup_Tree.Select[A])
    1.18      : Stream[Text.Info[Option[A]]] =
    1.19    {
    1.20      def stream(