special treatment for various kinds of selections: imitate normal flow of editing;
authorwenzelm
Sun Mar 30 20:23:26 2014 +0200 (2014-03-30 ago)
changeset 56325ffbfc92e6508
parent 56324 f9de5e5b56e6
child 56326 c3d7b3bb2708
special treatment for various kinds of selections: imitate normal flow of editing;
src/Tools/jEdit/src/completion_popup.scala
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Sat Mar 29 21:26:11 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Sun Mar 30 20:23:26 2014 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4  import scala.swing.event.MouseClicked
     1.5  
     1.6  import org.gjt.sp.jedit.View
     1.7 -import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
     1.8 +import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, Selection}
     1.9  import org.gjt.sp.jedit.gui.{HistoryTextField, KeyEventWorkaround}
    1.10  
    1.11  
    1.12 @@ -200,9 +200,31 @@
    1.13          JEdit_Lib.buffer_edit(buffer) {
    1.14            JEdit_Lib.try_get_text(buffer, range) match {
    1.15              case Some(text) if text == item.original =>
    1.16 -              buffer.remove(range.start, range.length)
    1.17 -              buffer.insert(range.start, item.replacement)
    1.18 -              text_area.moveCaretPosition(range.start + item.replacement.length + item.move)
    1.19 +              text_area.getSelectionAtOffset(text_area.getCaretPosition) match {
    1.20 +
    1.21 +                /*rectangular selection as "tall caret"*/
    1.22 +                case selection : Selection.Rect
    1.23 +                if selection.getStart(buffer, text_area.getCaretLine) == range.stop =>
    1.24 +                  text_area.moveCaretPosition(range.stop)
    1.25 +                  (0 until Character.codePointCount(item.original, 0, item.original.length))
    1.26 +                    .foreach(_ => text_area.backspace())
    1.27 +                  text_area.setSelectedText(selection, item.replacement)
    1.28 +                  text_area.moveCaretPosition(text_area.getCaretPosition + item.move)
    1.29 +
    1.30 +                /*other selections: rectangular, multiple range, ...*/
    1.31 +                case selection
    1.32 +                if selection != null &&
    1.33 +                    selection.getStart(buffer, text_area.getCaretLine) == range.start &&
    1.34 +                    selection.getEnd(buffer, text_area.getCaretLine) == range.stop =>
    1.35 +                  text_area.moveCaretPosition(range.stop + item.move)
    1.36 +                  text_area.getSelection.foreach(text_area.setSelectedText(_, item.replacement))
    1.37 +
    1.38 +                /*no selection*/
    1.39 +                case _ =>
    1.40 +                  buffer.remove(range.start, range.length)
    1.41 +                  buffer.insert(range.start, item.replacement)
    1.42 +                  text_area.moveCaretPosition(range.start + item.replacement.length + item.move)
    1.43 +              }
    1.44              case _ =>
    1.45            }
    1.46          }