--- a/src/Tools/jEdit/src/token_markup.scala Sun Nov 25 21:40:34 2012 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala Mon Nov 26 10:37:05 2012 +0100
@@ -48,13 +48,7 @@
val buffer = text_area.getBuffer
text_area.getSelection.toList match {
- case Nil if control == "" =>
- JEdit_Lib.buffer_edit(buffer) {
- val caret = text_area.getCaretPosition
- if (caret > 0 && is_control_style(buffer.getText(caret - 1, 1)))
- text_area.backspace()
- }
- case Nil if control != "" =>
+ case Nil =>
text_area.setSelectedText(control)
case sels =>
JEdit_Lib.buffer_edit(buffer) {