src/Pure/PIDE/document.scala

--- a/src/Pure/PIDE/document.scala	Tue Sep 07 22:28:58 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Sep 07 23:06:52 2010 +0200
@@ -172,7 +172,7 @@
     def convert(range: Text.Range): Text.Range
     def revert(i: Text.Offset): Text.Offset
     def revert(range: Text.Range): Text.Range
-    def select_markup[A](range: Text.Range)(result: PartialFunction[Text.Info[Any], A])
+    def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A])
       : Stream[Text.Info[Option[A]]]
   }
 
@@ -310,7 +310,7 @@
         def revert(range: Text.Range): Text.Range =
           if (edits.isEmpty) range else range.map(revert(_))
 
-        def select_markup[A](range: Text.Range)(result: PartialFunction[Text.Info[Any], A])
+        def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A])
           : Stream[Text.Info[Option[A]]] =
         {
           val former_range = revert(range)