src/Tools/jEdit/src/pretty_text_area.scala

 
   addKeyListener(JEdit_Lib.key_listener(
     key_pressed = (evt: KeyEvent) =>
       {
         evt.getKeyCode match {
-          case KeyEvent.VK_C
+          case KeyEvent.VK_C | KeyEvent.VK_INSERT
           if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 &&
               text_area.getSelectionCount != 0 =>
             Registers.copy(text_area, '$')
             evt.consume