src/Pure/PIDE/text.scala

--- a/src/Pure/PIDE/text.scala	Sat Jan 14 13:22:39 2012 +0100
+++ b/src/Pure/PIDE/text.scala	Sat Jan 14 14:34:42 2012 +0100
@@ -118,9 +118,7 @@
   sealed 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 ERROR(_) => None }
+    def try_restrict(r: Text.Range): Option[Info[A]] = range.try_restrict(r).map(Info(_, info))
   }
 
   type Markup = Info[XML.Elem]