src/Tools/jEdit/src/pretty_text_area.scala
changeset 56323 e925118b1875
parent 55826 e56a52dd770a
child 56360 1d122af2b11a
equal deleted inserted replaced
56322:f9ad26836516 56323:e925118b1875
   164   addKeyListener(JEdit_Lib.key_listener(
   164   addKeyListener(JEdit_Lib.key_listener(
   165     key_pressed = (evt: KeyEvent) =>
   165     key_pressed = (evt: KeyEvent) =>
   166       {
   166       {
   167         evt.getKeyCode match {
   167         evt.getKeyCode match {
   168           case KeyEvent.VK_C
   168           case KeyEvent.VK_C
   169           if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 =>
   169           if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 &&
       
   170               text_area.getSelectionCount != 0 =>
   170             Registers.copy(text_area, '$')
   171             Registers.copy(text_area, '$')
   171             evt.consume
   172             evt.consume
   172 
   173 
   173           case KeyEvent.VK_A
   174           case KeyEvent.VK_A
   174           if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 =>
   175           if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 =>