src/Tools/jEdit/src/completion_popup.scala
changeset 53237 6bfe54791591
parent 53236 837a6ef61fe9
child 53242 142f4fff4e40
equal deleted inserted replaced
53236:837a6ef61fe9 53237:6bfe54791591
   184 
   184 
   185   /* event handling */
   185   /* event handling */
   186 
   186 
   187   private val key_listener =
   187   private val key_listener =
   188     JEdit_Lib.key_listener(
   188     JEdit_Lib.key_listener(
   189       workaround = false,
       
   190       key_pressed = (e: KeyEvent) =>
   189       key_pressed = (e: KeyEvent) =>
   191         {
   190         {
   192           if (!e.isConsumed) {
   191           if (!e.isConsumed) {
   193             e.getKeyCode match {
   192             e.getKeyCode match {
   194               case KeyEvent.VK_TAB =>
   193               case KeyEvent.VK_TAB =>