src/Pure/PIDE/document.scala

     def state(command: Command): Command.State
     def convert(i: Text.Offset): Text.Offset
     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]]]
   }
 
   object State
   {

           if (edits.isEmpty) range else range.map(convert(_))
 
         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)
           for {
             (command, command_start) <- node.command_range(former_range).toStream