src/Pure/PIDE/markup_tree.scala

--- a/src/Pure/PIDE/markup_tree.scala	Tue Sep 07 22:28:58 2010 +0200
+++ b/src/Pure/PIDE/markup_tree.scala	Tue Sep 07 23:06:52 2010 +0200
@@ -43,6 +43,8 @@
   }
 
   val empty = new Markup_Tree(Branches.empty)
+
+  type Select[A] = PartialFunction[Text.Info[Any], A]
 }
 
 
@@ -89,7 +91,7 @@
   private def overlapping(range: Text.Range): Stream[(Text.Range, Branches.Entry)] =
     Branches.overlapping(range, branches).toStream
 
-  def select[A](root_range: Text.Range)(result: PartialFunction[Text.Info[Any], A])
+  def select[A](root_range: Text.Range)(result: Markup_Tree.Select[A])
     : Stream[Text.Info[Option[A]]] =
   {
     def stream(