# HG changeset patch
# User wenzelm
# Date 1397573046 -7200
# Node ID d01d183e84eabfb7b43aadeee5c8282f94591d94
# Parent  71c5d1f516c0e5b6795f4c0d5a505d74e2b8502b
clarified treatment of markup ranges wrt. revert/convert: inflate_singularity allows to retrieve information like language_context more reliably during editing;

diff -r 71c5d1f516c0 -r d01d183e84ea src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Apr 15 13:07:59 2014 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Apr 15 16:44:06 2014 +0200
@@ -773,7 +773,7 @@
           result: List[Command.State] => (A, Text.Markup) => Option[A],
           status: Boolean = false): List[Text.Info[A]] =
         {
-          val former_range = revert(range)
+          val former_range = revert(range).inflate_singularity
           val (chunk_name, command_iterator) =
             load_commands match {
               case command :: _ => (Text.Chunk.File(node_name.node), Iterator((command, 0)))
@@ -785,13 +785,14 @@
             chunk <- command.chunks.get(chunk_name).iterator
             states = state.command_states(version, command)
             res = result(states)
-            range = (former_range - command_start).restrict(chunk.range)
-            markup = Command.State.merge_markup(states, markup_index, range, elements)
-            Text.Info(r0, a) <- markup.cumulate[A](range, info, elements,
+            markup_range <- (former_range - command_start).try_restrict(chunk.range).iterator
+            markup = Command.State.merge_markup(states, markup_index, markup_range, elements)
+            Text.Info(r0, a) <- markup.cumulate[A](markup_range, info, elements,
               {
                 case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b))
               }).iterator
-          } yield Text.Info(convert(r0 + command_start), a)).toList
+            r1 <- convert(r0 + command_start).try_restrict(range).iterator
+          } yield Text.Info(r1, a)).toList
         }
 
         def select[A](
diff -r 71c5d1f516c0 -r d01d183e84ea src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Tue Apr 15 13:07:59 2014 +0200
+++ b/src/Pure/PIDE/text.scala	Tue Apr 15 16:44:06 2014 +0200
@@ -49,6 +49,7 @@
     def -(i: Offset): Range = if (i == 0) this else map(_ - i)
 
     def is_singularity: Boolean = start == stop
+    def inflate_singularity: Range = if (is_singularity) Range(start, start + 1) else this
 
     def contains(i: Offset): Boolean = start == i || start < i && i < stop
     def contains(that: Range): Boolean = this.contains(that.start) && that.stop <= this.stop