clarified partial restrict operation;
authorwenzelm
Sat Jan 14 14:34:42 2012 +0100 (2012-01-14)
changeset 46207e76b77356ed6
parent 46206 d3d62b528487
child 46208 4cab63a6dc16
clarified partial restrict operation;
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/text.scala
     1.1 --- a/src/Pure/PIDE/protocol.scala	Sat Jan 14 13:22:39 2012 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Sat Jan 14 14:34:42 2012 +0100
     1.3 @@ -148,6 +148,7 @@
     1.4        tree match {
     1.5          case XML.Elem(Markup(name, Position.Id_Range(id, raw_range)), body)
     1.6          if include_pos(name) && id == command.id =>
     1.7 +          // FIXME handle message range outside command range (!??!)
     1.8            val range = command.decode(raw_range).restrict(command.range)
     1.9            body.foldLeft(if (range.is_singularity) set else set + range)(positions)
    1.10          case XML.Elem(Markup(name, _), body) => body.foldLeft(set)(positions)
     2.1 --- a/src/Pure/PIDE/text.scala	Sat Jan 14 13:22:39 2012 +0100
     2.2 +++ b/src/Pure/PIDE/text.scala	Sat Jan 14 14:34:42 2012 +0100
     2.3 @@ -118,9 +118,7 @@
     2.4    sealed case class Info[A](val range: Text.Range, val info: A)
     2.5    {
     2.6      def restrict(r: Text.Range): Info[A] = Info(range.restrict(r), info)
     2.7 -    def try_restrict(r: Text.Range): Option[Info[A]] =
     2.8 -      try { Some(Info(range.restrict(r), info)) }
     2.9 -      catch { case ERROR(_) => None }
    2.10 +    def try_restrict(r: Text.Range): Option[Info[A]] = range.try_restrict(r).map(Info(_, info))
    2.11    }
    2.12  
    2.13    type Markup = Info[XML.Elem]