equal
deleted
inserted
replaced
700 JEdit_Lib.key_listener( |
700 JEdit_Lib.key_listener( |
701 key_pressed = (e: KeyEvent) => |
701 key_pressed = (e: KeyEvent) => |
702 { |
702 { |
703 if (!e.isConsumed) { |
703 if (!e.isConsumed) { |
704 e.getKeyCode match { |
704 e.getKeyCode match { |
705 case KeyEvent.VK_TAB => |
705 case KeyEvent.VK_ENTER if PIDE.options.bool("jedit_completion_select_enter") => |
|
706 if (complete_selected()) e.consume |
|
707 hide_popup() |
|
708 case KeyEvent.VK_TAB if PIDE.options.bool("jedit_completion_select_tab") => |
706 if (complete_selected()) e.consume |
709 if (complete_selected()) e.consume |
707 hide_popup() |
710 hide_popup() |
708 case KeyEvent.VK_ESCAPE => |
711 case KeyEvent.VK_ESCAPE => |
709 hide_popup() |
712 hide_popup() |
710 e.consume |
713 e.consume |