# HG changeset patch # User wenzelm # Date 1353922625 -3600 # Node ID 747db833fbf76b53b617c2b7e19cccb9dd8bf793 # Parent 907373a080b997eea0859d22fb6146e2495795da no special treatment of control_reset, in accordance to other control styles; diff -r 907373a080b9 -r 747db833fbf7 src/Tools/jEdit/src/token_markup.scala --- 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) {