src/Tools/jEdit/src/completion_popup.scala

 
     def active_range: Option[Text.Range] =
       completion_popup match {
         case Some(completion) =>
           completion.active_range match {
-            case Some((range, _)) if completion.isDisplayable => Some(range)
+            case Some(range) if completion.isDisplayable => Some(range)
             case _ => None
           }
         case None => None
       }
 

             SwingUtilities.convertPoint(painter,
               loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
 
           val items = result.items.map(new Item(_))
           val completion =
-            new Completion_Popup(Some((range, invalidate _)), layered, loc2, font, items)
+            new Completion_Popup(Some(range), layered, loc2, font, items)
             {
               override def complete(item: Completion.Item) {
                 PIDE.completion_history.update(item)
                 insert(item)
               }
               override def propagate(evt: KeyEvent) {
-                JEdit_Lib.propagate_key(view, evt)
+                if (view.getKeyEventInterceptor == inner_key_listener) {
+                  try {
+                    view.setKeyEventInterceptor(null)
+                    JEdit_Lib.propagate_key(view, evt)
+                  }
+                  finally {
+                    if (isDisplayable) view.setKeyEventInterceptor(inner_key_listener)
+                  }
+                }
                 if (evt.getID == KeyEvent.KEY_TYPED) input(evt)
               }
-              override def refocus() { text_area.requestFocus }
+              override def shutdown(focus: Boolean) {
+                if (view.getKeyEventInterceptor == inner_key_listener)
+                  view.setKeyEventInterceptor(null)
+                if (focus) text_area.requestFocus
+                invalidate()
+              }
             }
           completion_popup = Some(completion)
+          view.setKeyEventInterceptor(completion.inner_key_listener)
           invalidate()
-          completion.show_popup()
+          completion.show_popup(false)
         }
       }
 
       if (buffer.isEditable) {
         val (no_completion, semantic_completion, opt_rendering) =

                     insert(item)
                   }
                   override def propagate(evt: KeyEvent) {
                     if (!evt.isConsumed) text_field.processKeyEvent(evt)
                   }
-                  override def refocus() { text_field.requestFocus }
+                  override def shutdown(focus: Boolean) { if (focus) text_field.requestFocus }
                 }
               completion_popup = Some(completion)
-              completion.show_popup()
+              completion.show_popup(true)
 
             case None =>
           }
         case _ =>
       }

   }
 }
 
 
 class Completion_Popup private(
-  val active_range: Option[(Text.Range, () => Unit)],
+  val active_range: Option[Text.Range],
   layered: JLayeredPane,
   location: Point,
   font: Font,
   items: List[Completion_Popup.Item]) extends JPanel(new BorderLayout)
 {

 
   /* actions */
 
   def complete(item: Completion.Item) { }
   def propagate(evt: KeyEvent) { }
-  def refocus() { }
+  def shutdown(focus: Boolean) { }
 
 
   /* list view */
 
   private val list_view = new ListView(items)

   }
 
 
   /* event handling */
 
-  private val inner_key_listener =
+  val inner_key_listener =
     JEdit_Lib.key_listener(
       key_pressed = (e: KeyEvent) =>
         {
           if (!e.isConsumed) {
             e.getKeyCode match {

       new Dimension(w, h)
     }
     new Popup(layered, completion, screen.relative(layered, size), size)
   }
 
-  private def show_popup()
+  private def show_popup(focus: Boolean)
   {
     popup.show
-    list_view.requestFocus
-  }
-
-  private val hide_popup_delay =
-    Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_dismiss_delay")) {
-      active_range match { case Some((_, invalidate)) => invalidate() case _ => }
-      popup.hide
-    }
+    if (focus) list_view.requestFocus
+  }
 
   private def hide_popup()
   {
-    if (list_view.peer.isFocusOwner) refocus()
-
-    if (PIDE.options.seconds("jedit_completion_dismiss_delay").is_zero) {
-      active_range match { case Some((_, invalidate)) => invalidate() case _ => }
-      popup.hide
-    }
-    else hide_popup_delay.invoke()
+    shutdown(list_view.peer.isFocusOwner)
+    popup.hide
   }
 }