--- 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)))
}
--- 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 =