src/Pure/PIDE/document.scala
changeset 56590 d01d183e84ea
parent 56514 db929027e701
child 56711 ef3d00153e3b
     1.1 --- a/src/Pure/PIDE/document.scala	Tue Apr 15 13:07:59 2014 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Tue Apr 15 16:44:06 2014 +0200
     1.3 @@ -773,7 +773,7 @@
     1.4            result: List[Command.State] => (A, Text.Markup) => Option[A],
     1.5            status: Boolean = false): List[Text.Info[A]] =
     1.6          {
     1.7 -          val former_range = revert(range)
     1.8 +          val former_range = revert(range).inflate_singularity
     1.9            val (chunk_name, command_iterator) =
    1.10              load_commands match {
    1.11                case command :: _ => (Text.Chunk.File(node_name.node), Iterator((command, 0)))
    1.12 @@ -785,13 +785,14 @@
    1.13              chunk <- command.chunks.get(chunk_name).iterator
    1.14              states = state.command_states(version, command)
    1.15              res = result(states)
    1.16 -            range = (former_range - command_start).restrict(chunk.range)
    1.17 -            markup = Command.State.merge_markup(states, markup_index, range, elements)
    1.18 -            Text.Info(r0, a) <- markup.cumulate[A](range, info, elements,
    1.19 +            markup_range <- (former_range - command_start).try_restrict(chunk.range).iterator
    1.20 +            markup = Command.State.merge_markup(states, markup_index, markup_range, elements)
    1.21 +            Text.Info(r0, a) <- markup.cumulate[A](markup_range, info, elements,
    1.22                {
    1.23                  case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b))
    1.24                }).iterator
    1.25 -          } yield Text.Info(convert(r0 + command_start), a)).toList
    1.26 +            r1 <- convert(r0 + command_start).try_restrict(range).iterator
    1.27 +          } yield Text.Info(r1, a)).toList
    1.28          }
    1.29  
    1.30          def select[A](