src/Pure/PIDE/document.scala

--- a/src/Pure/PIDE/document.scala	Sat Aug 28 22:58:24 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Sun Aug 29 15:09:11 2010 +0200
@@ -147,6 +147,8 @@
     def convert(range: Text.Range): Text.Range = range.map(convert(_))
     def revert(i: Text.Offset): Text.Offset
     def revert(range: Text.Range): Text.Range = range.map(revert(_))
+    def select_markup[A](range: Text.Range)
+      (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]]
   }
 
   object State
@@ -275,6 +277,23 @@
 
         def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
         def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
+
+        def select_markup[A](range: Text.Range)
+          (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]] =
+        {
+          val former_range = revert(range)
+          for {
+            (command, command_start) <- node.command_range(former_range)
+            Text.Info(r0, x) <- state(command).markup.
+              select((former_range - command_start).restrict(command.range)) {
+                case Text.Info(r0, info)
+                if result.isDefinedAt(Text.Info(convert(r0 + command_start), info)) =>
+                  result(Text.Info(convert(r0 + command_start), info))
+              } { default }
+            val r = convert(r0 + command_start)
+            if !r.is_singularity
+          } yield Text.Info(r, x)
+        }
       }
     }
   }