clarified treatment of markup ranges wrt. revert/convert: inflate_singularity allows to retrieve information like language_context more reliably during editing;
authorwenzelm
Tue Apr 15 16:44:06 2014 +0200 (2014-04-15)
changeset 56590d01d183e84ea
parent 56589 71c5d1f516c0
child 56591 1a59587f46ec
clarified treatment of markup ranges wrt. revert/convert: inflate_singularity allows to retrieve information like language_context more reliably during editing;
src/Pure/PIDE/document.scala
src/Pure/PIDE/text.scala
     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