src/Pure/PIDE/text.scala
changeset 43428 b41dea5772c6
parent 43425 0a5612040a8b
child 43650 f00da558b78e
     1.1 --- a/src/Pure/PIDE/text.scala	Sat Jun 18 00:03:58 2011 +0200
     1.2 +++ b/src/Pure/PIDE/text.scala	Sat Jun 18 00:05:29 2011 +0200
     1.3 @@ -43,6 +43,10 @@
     1.4  
     1.5      def restrict(that: Range): Range =
     1.6        Range(this.start max that.start, this.stop min that.stop)
     1.7 +
     1.8 +    def try_restrict(that: Range): Option[Range] =
     1.9 +      try { Some (restrict(that)) }
    1.10 +      catch { case _: RuntimeException => None }
    1.11    }
    1.12  
    1.13  
    1.14 @@ -51,6 +55,9 @@
    1.15    case class Info[A](val range: Text.Range, val info: A)
    1.16    {
    1.17      def restrict(r: Text.Range): Info[A] = Info(range.restrict(r), info)
    1.18 +    def try_restrict(r: Text.Range): Option[Info[A]] =
    1.19 +      try { Some(Info(range.restrict(r), info)) }
    1.20 +      catch { case _: RuntimeException => None }
    1.21    }
    1.22  
    1.23