# HG changeset patch # User wenzelm # Date 1396203806 -7200 # Node ID ffbfc92e6508073a9254b53bdba12d32574b3bee # Parent f9de5e5b56e6f5ef564b9d64a8627d8753114457 special treatment for various kinds of selections: imitate normal flow of editing; diff -r f9de5e5b56e6 -r ffbfc92e6508 src/Tools/jEdit/src/completion_popup.scala --- a/src/Tools/jEdit/src/completion_popup.scala Sat Mar 29 21:26:11 2014 +0100 +++ b/src/Tools/jEdit/src/completion_popup.scala Sun Mar 30 20:23:26 2014 +0200 @@ -19,7 +19,7 @@ import scala.swing.event.MouseClicked import org.gjt.sp.jedit.View -import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea} +import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, Selection} import org.gjt.sp.jedit.gui.{HistoryTextField, KeyEventWorkaround} @@ -200,9 +200,31 @@ JEdit_Lib.buffer_edit(buffer) { JEdit_Lib.try_get_text(buffer, range) match { case Some(text) if text == item.original => - buffer.remove(range.start, range.length) - buffer.insert(range.start, item.replacement) - text_area.moveCaretPosition(range.start + item.replacement.length + item.move) + text_area.getSelectionAtOffset(text_area.getCaretPosition) match { + + /*rectangular selection as "tall caret"*/ + case selection : Selection.Rect + if selection.getStart(buffer, text_area.getCaretLine) == range.stop => + text_area.moveCaretPosition(range.stop) + (0 until Character.codePointCount(item.original, 0, item.original.length)) + .foreach(_ => text_area.backspace()) + text_area.setSelectedText(selection, item.replacement) + text_area.moveCaretPosition(text_area.getCaretPosition + item.move) + + /*other selections: rectangular, multiple range, ...*/ + case selection + if selection != null && + selection.getStart(buffer, text_area.getCaretLine) == range.start && + selection.getEnd(buffer, text_area.getCaretLine) == range.stop => + text_area.moveCaretPosition(range.stop + item.move) + text_area.getSelection.foreach(text_area.setSelectedText(_, item.replacement)) + + /*no selection*/ + case _ => + buffer.remove(range.start, range.length) + buffer.insert(range.start, item.replacement) + text_area.moveCaretPosition(range.start + item.replacement.length + item.move) + } case _ => } }