# HG changeset patch
# User wenzelm
# Date 1393180167 -3600
# Node ID 19e8b00684f782286c9f22fa9e05bb2276811fef
# Parent  aeba7cd454000a896feda724910c130a4e623317
more explicit Completion.Item.range, independently of caret;

diff -r aeba7cd45400 -r 19e8b00684f7 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Sun Feb 23 18:18:40 2014 +0100
+++ b/src/Pure/General/completion.scala	Sun Feb 23 19:29:27 2014 +0100
@@ -56,6 +56,7 @@
   /* result */
 
   sealed case class Item(
+    range: Text.Range,
     original: String,
     name: String,
     replacement: String,
@@ -240,6 +241,7 @@
     history: Completion.History,
     decode: Boolean,
     explicit: Boolean,
+    text_start: Text.Offset,
     text: CharSequence,
     context: Completion.Context): Option[Completion.Result] =
   {
@@ -289,7 +291,8 @@
                   case List(s1, s2) => (s1, s2)
                   case _ => (s, "")
                 }
-              Completion.Item(word, s, s1 + s2, - s2.length, explicit || immediate)
+              val range = Text.Range(- word.length, 0) + (text_start + text.length)
+              Completion.Item(range, word, s, s1 + s2, - s2.length, explicit || immediate)
             })
           Some(Completion.Result(word, cs.length == 1, items.sorted(history.ordering)))
         }
diff -r aeba7cd45400 -r 19e8b00684f7 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Sun Feb 23 18:18:40 2014 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala	Sun Feb 23 19:29:27 2014 +0100
@@ -79,16 +79,14 @@
       Swing_Thread.require()
 
       val buffer = text_area.getBuffer
-      val len = item.original.length
-      if (buffer.isEditable && len > 0) {
+      val range = item.range
+      if (buffer.isEditable && range.length > 0) {
         JEdit_Lib.buffer_edit(buffer) {
-          val caret = text_area.getCaretPosition
-          JEdit_Lib.try_get_text(buffer, Text.Range(caret - len, caret)) match {
+          JEdit_Lib.try_get_text(buffer, range) match {
             case Some(text) if text == item.original =>
-              buffer.remove(caret - len, len)
-              buffer.insert(caret - len, item.replacement)
-              if (item.move != 0)
-                text_area.moveCaretPosition(text_area.getCaretPosition + item.move)
+              buffer.remove(range.start, range.length)
+              buffer.insert(range.start, item.replacement)
+              text_area.moveCaretPosition(range.start + item.replacement.length + item.move)
             case _ =>
           }
         }
@@ -120,7 +118,7 @@
                   rendering.completion_context(JEdit_Lib.stretch_point_range(buffer, caret))
               }) getOrElse syntax.completion_context
 
-            syntax.completion.complete(history, decode, explicit, text, context) match {
+            syntax.completion.complete(history, decode, explicit, start, text, context) match {
               case Some(result) =>
                 if (result.unique && result.items.head.immediate && immediate)
                   insert(result.items.head)
@@ -259,17 +257,16 @@
     {
       Swing_Thread.require()
 
-      val len = item.original.length
-      if (text_field.isEditable && len > 0) {
-        val caret = text_field.getCaret.getDot
+      val range = item.range
+      if (text_field.isEditable && range.length > 0) {
         val content = text_field.getText
-        JEdit_Lib.try_get_text(content, Text.Range(caret - len, caret)) match {
+        JEdit_Lib.try_get_text(content, range) match {
           case Some(text) if text == item.original =>
             text_field.setText(
-              content.substring(0, caret - len) +
+              content.substring(0, range.start) +
               item.replacement +
-              content.substring(caret))
-            text_field.getCaret.setDot(caret - len + item.replacement.length + item.move)
+              content.substring(range.stop))
+            text_field.getCaret.setDot(range.start + item.replacement.length + item.move)
           case _ =>
         }
       }
@@ -288,7 +285,7 @@
           val text = text_field.getText.substring(0, caret)
 
           syntax.completion.complete(
-              history, decode = true, explicit = false, text, syntax.completion_context) match {
+              history, decode = true, explicit = false, 0, text, syntax.completion_context) match {
             case Some(result) =>
               val fm = text_field.getFontMetrics(text_field.getFont)
               val loc =