# HG changeset patch # User wenzelm # Date 1378290000 -7200 # Node ID f8b150e8778b47b02b90852fbeb7a19a841487c2 # Parent b179cdfa9d82c8ba06eb39af9ebf21390641f377 remove Swing input map, which might bind keys in unexpected ways (e.g. LEFT/RIGHT in singleton list); handle KP_UP/KP_DOWN keys as well, like Swing does; diff -r b179cdfa9d82 -r f8b150e8778b NEWS --- a/NEWS Wed Sep 04 11:12:00 2013 +0200 +++ b/NEWS Wed Sep 04 12:20:00 2013 +0200 @@ -101,7 +101,7 @@ - Light-weight popup, which avoids explicit window (more reactive and more robust). Interpreted key events include TAB, ESCAPE, UP, - DOWN, PAGE_UP, PAGE_DOWN. Uninterpreted key events are passed to + DOWN, PAGE_UP, PAGE_DOWN. All other key events are passed to the jEdit text area. - Explicit completion via standard jEdit shortcut C+b, which has diff -r b179cdfa9d82 -r f8b150e8778b src/Tools/jEdit/src/completion_popup.scala --- a/src/Tools/jEdit/src/completion_popup.scala Wed Sep 04 11:12:00 2013 +0200 +++ b/src/Tools/jEdit/src/completion_popup.scala Wed Sep 04 12:20:00 2013 +0200 @@ -244,6 +244,11 @@ list_view.peer.setVisibleRowCount(items.length min 8) list_view.peer.setSelectedIndex(0) + for (cond <- + List(JComponent.WHEN_FOCUSED, + JComponent.WHEN_ANCESTOR_OF_FOCUSED_COMPONENT, + JComponent.WHEN_IN_FOCUSED_WINDOW)) list_view.peer.setInputMap(cond, null) + private def complete_selected(): Boolean = { list_view.selection.items.toList match { @@ -283,8 +288,8 @@ case KeyEvent.VK_ESCAPE => hide_popup() e.consume - case KeyEvent.VK_UP => move_items(-1); e.consume - case KeyEvent.VK_DOWN => move_items(1); e.consume + case KeyEvent.VK_UP | KeyEvent.VK_KP_UP => move_items(-1); e.consume + case KeyEvent.VK_DOWN | KeyEvent.VK_KP_DOWN => move_items(1); e.consume case KeyEvent.VK_PAGE_UP => move_pages(-1); e.consume case KeyEvent.VK_PAGE_DOWN => move_pages(1); e.consume case _ =>