clarified treatment of markup ranges wrt. revert/convert: inflate_singularity allows to retrieve information like language_context more reliably during editing;
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](
2.1 --- a/src/Pure/PIDE/text.scala Tue Apr 15 13:07:59 2014 +0200
2.2 +++ b/src/Pure/PIDE/text.scala Tue Apr 15 16:44:06 2014 +0200
2.3 @@ -49,6 +49,7 @@
2.4 def -(i: Offset): Range = if (i == 0) this else map(_ - i)
2.5
2.6 def is_singularity: Boolean = start == stop
2.7 + def inflate_singularity: Range = if (is_singularity) Range(start, start + 1) else this
2.8
2.9 def contains(i: Offset): Boolean = start == i || start < i && i < stop
2.10 def contains(that: Range): Boolean = this.contains(that.start) && that.stop <= this.stop