src/Pure/PIDE/text.scala

--- a/src/Pure/PIDE/text.scala	Sat Jun 18 00:03:58 2011 +0200
+++ b/src/Pure/PIDE/text.scala	Sat Jun 18 00:05:29 2011 +0200
@@ -43,6 +43,10 @@
 
     def restrict(that: Range): Range =
       Range(this.start max that.start, this.stop min that.stop)
+
+    def try_restrict(that: Range): Option[Range] =
+      try { Some (restrict(that)) }
+      catch { case _: RuntimeException => None }
   }
 
 
@@ -51,6 +55,9 @@
   case class Info[A](val range: Text.Range, val info: A)
   {
     def restrict(r: Text.Range): Info[A] = Info(range.restrict(r), info)
+    def try_restrict(r: Text.Range): Option[Info[A]] =
+      try { Some(Info(range.restrict(r), info)) }
+      catch { case _: RuntimeException => None }
   }