src/Pure/PIDE/text.scala
changeset 43650 f00da558b78e
parent 43428 b41dea5772c6
child 43714 3749d1e6dde9
     1.1 --- a/src/Pure/PIDE/text.scala	Sun Jul 03 19:53:35 2011 +0200
     1.2 +++ b/src/Pure/PIDE/text.scala	Mon Jul 04 13:43:10 2011 +0200
     1.3 @@ -46,7 +46,7 @@
     1.4  
     1.5      def try_restrict(that: Range): Option[Range] =
     1.6        try { Some (restrict(that)) }
     1.7 -      catch { case _: RuntimeException => None }
     1.8 +      catch { case ERROR(_) => None }
     1.9    }
    1.10  
    1.11  
    1.12 @@ -57,7 +57,7 @@
    1.13      def restrict(r: Text.Range): Info[A] = Info(range.restrict(r), info)
    1.14      def try_restrict(r: Text.Range): Option[Info[A]] =
    1.15        try { Some(Info(range.restrict(r), info)) }
    1.16 -      catch { case _: RuntimeException => None }
    1.17 +      catch { case ERROR(_) => None }
    1.18    }
    1.19  
    1.20