more explicit Completion.Item.range, independently of caret;
authorwenzelm
Sun Feb 23 19:29:27 2014 +0100 (2014-02-23 ago)
changeset 5569219e8b00684f7
parent 55691 aeba7cd45400
child 55693 93ba0085e888
more explicit Completion.Item.range, independently of caret;
src/Pure/General/completion.scala
src/Tools/jEdit/src/completion_popup.scala
     1.1 --- a/src/Pure/General/completion.scala	Sun Feb 23 18:18:40 2014 +0100
     1.2 +++ b/src/Pure/General/completion.scala	Sun Feb 23 19:29:27 2014 +0100
     1.3 @@ -56,6 +56,7 @@
     1.4    /* result */
     1.5  
     1.6    sealed case class Item(
     1.7 +    range: Text.Range,
     1.8      original: String,
     1.9      name: String,
    1.10      replacement: String,
    1.11 @@ -240,6 +241,7 @@
    1.12      history: Completion.History,
    1.13      decode: Boolean,
    1.14      explicit: Boolean,
    1.15 +    text_start: Text.Offset,
    1.16      text: CharSequence,
    1.17      context: Completion.Context): Option[Completion.Result] =
    1.18    {
    1.19 @@ -289,7 +291,8 @@
    1.20                    case List(s1, s2) => (s1, s2)
    1.21                    case _ => (s, "")
    1.22                  }
    1.23 -              Completion.Item(word, s, s1 + s2, - s2.length, explicit || immediate)
    1.24 +              val range = Text.Range(- word.length, 0) + (text_start + text.length)
    1.25 +              Completion.Item(range, word, s, s1 + s2, - s2.length, explicit || immediate)
    1.26              })
    1.27            Some(Completion.Result(word, cs.length == 1, items.sorted(history.ordering)))
    1.28          }
     2.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Sun Feb 23 18:18:40 2014 +0100
     2.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Sun Feb 23 19:29:27 2014 +0100
     2.3 @@ -79,16 +79,14 @@
     2.4        Swing_Thread.require()
     2.5  
     2.6        val buffer = text_area.getBuffer
     2.7 -      val len = item.original.length
     2.8 -      if (buffer.isEditable && len > 0) {
     2.9 +      val range = item.range
    2.10 +      if (buffer.isEditable && range.length > 0) {
    2.11          JEdit_Lib.buffer_edit(buffer) {
    2.12 -          val caret = text_area.getCaretPosition
    2.13 -          JEdit_Lib.try_get_text(buffer, Text.Range(caret - len, caret)) match {
    2.14 +          JEdit_Lib.try_get_text(buffer, range) match {
    2.15              case Some(text) if text == item.original =>
    2.16 -              buffer.remove(caret - len, len)
    2.17 -              buffer.insert(caret - len, item.replacement)
    2.18 -              if (item.move != 0)
    2.19 -                text_area.moveCaretPosition(text_area.getCaretPosition + item.move)
    2.20 +              buffer.remove(range.start, range.length)
    2.21 +              buffer.insert(range.start, item.replacement)
    2.22 +              text_area.moveCaretPosition(range.start + item.replacement.length + item.move)
    2.23              case _ =>
    2.24            }
    2.25          }
    2.26 @@ -120,7 +118,7 @@
    2.27                    rendering.completion_context(JEdit_Lib.stretch_point_range(buffer, caret))
    2.28                }) getOrElse syntax.completion_context
    2.29  
    2.30 -            syntax.completion.complete(history, decode, explicit, text, context) match {
    2.31 +            syntax.completion.complete(history, decode, explicit, start, text, context) match {
    2.32                case Some(result) =>
    2.33                  if (result.unique && result.items.head.immediate && immediate)
    2.34                    insert(result.items.head)
    2.35 @@ -259,17 +257,16 @@
    2.36      {
    2.37        Swing_Thread.require()
    2.38  
    2.39 -      val len = item.original.length
    2.40 -      if (text_field.isEditable && len > 0) {
    2.41 -        val caret = text_field.getCaret.getDot
    2.42 +      val range = item.range
    2.43 +      if (text_field.isEditable && range.length > 0) {
    2.44          val content = text_field.getText
    2.45 -        JEdit_Lib.try_get_text(content, Text.Range(caret - len, caret)) match {
    2.46 +        JEdit_Lib.try_get_text(content, range) match {
    2.47            case Some(text) if text == item.original =>
    2.48              text_field.setText(
    2.49 -              content.substring(0, caret - len) +
    2.50 +              content.substring(0, range.start) +
    2.51                item.replacement +
    2.52 -              content.substring(caret))
    2.53 -            text_field.getCaret.setDot(caret - len + item.replacement.length + item.move)
    2.54 +              content.substring(range.stop))
    2.55 +            text_field.getCaret.setDot(range.start + item.replacement.length + item.move)
    2.56            case _ =>
    2.57          }
    2.58        }
    2.59 @@ -288,7 +285,7 @@
    2.60            val text = text_field.getText.substring(0, caret)
    2.61  
    2.62            syntax.completion.complete(
    2.63 -              history, decode = true, explicit = false, text, syntax.completion_context) match {
    2.64 +              history, decode = true, explicit = false, 0, text, syntax.completion_context) match {
    2.65              case Some(result) =>
    2.66                val fm = text_field.getFontMetrics(text_field.getFont)
    2.67                val loc =