--- 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 }
}