src/Tools/jEdit/src/token_markup.scala
changeset 50210 747db833fbf7
parent 50205 788c8263e634
child 50663 f8d7d332fec0
equal deleted inserted replaced
50209:907373a080b9 50210:747db833fbf7
    46     Swing_Thread.assert()
    46     Swing_Thread.assert()
    47 
    47 
    48     val buffer = text_area.getBuffer
    48     val buffer = text_area.getBuffer
    49 
    49 
    50     text_area.getSelection.toList match {
    50     text_area.getSelection.toList match {
    51       case Nil if control == "" =>
    51       case Nil =>
    52         JEdit_Lib.buffer_edit(buffer) {
       
    53           val caret = text_area.getCaretPosition
       
    54           if (caret > 0 && is_control_style(buffer.getText(caret - 1, 1)))
       
    55             text_area.backspace()
       
    56         }
       
    57       case Nil if control != "" =>
       
    58         text_area.setSelectedText(control)
    52         text_area.setSelectedText(control)
    59       case sels =>
    53       case sels =>
    60         JEdit_Lib.buffer_edit(buffer) {
    54         JEdit_Lib.buffer_edit(buffer) {
    61           sels.foreach(sel =>
    55           sels.foreach(sel =>
    62             text_area.setSelectedText(sel,
    56             text_area.setSelectedText(sel,