src/Pure/PIDE/text.scala

--- a/src/Pure/PIDE/text.scala	Sun Jul 03 19:53:35 2011 +0200
+++ b/src/Pure/PIDE/text.scala	Mon Jul 04 13:43:10 2011 +0200
@@ -46,7 +46,7 @@
 
     def try_restrict(that: Range): Option[Range] =
       try { Some (restrict(that)) }
-      catch { case _: RuntimeException => None }
+      catch { case ERROR(_) => None }
   }
 
 
@@ -57,7 +57,7 @@
     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 }
+      catch { case ERROR(_) => None }
   }