# HG changeset patch
# User wenzelm
# Date 1326548082 -3600
# Node ID e76b77356ed6aff2359b6f29d0aa8ccd49b58840
# Parent  d3d62b528487293d6ff230911f21b60b5e35f430
clarified partial restrict operation;

diff -r d3d62b528487 -r e76b77356ed6 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Sat Jan 14 13:22:39 2012 +0100
+++ b/src/Pure/PIDE/protocol.scala	Sat Jan 14 14:34:42 2012 +0100
@@ -148,6 +148,7 @@
       tree match {
         case XML.Elem(Markup(name, Position.Id_Range(id, raw_range)), body)
         if include_pos(name) && id == command.id =>
+          // FIXME handle message range outside command range (!??!)
           val range = command.decode(raw_range).restrict(command.range)
           body.foldLeft(if (range.is_singularity) set else set + range)(positions)
         case XML.Elem(Markup(name, _), body) => body.foldLeft(set)(positions)
diff -r d3d62b528487 -r e76b77356ed6 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]