# 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) {