back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups;
authorwenzelm
Mon, 17 Mar 2014 23:16:26 +0100
changeset 56197 416f7a00e4cb
parent 56187 2666cd7d380c
child 56198 21dd034523e5
back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups; discontinued obsolete option jedit_completion_dismiss_delay (see 750561986828); more explicit shutdown;
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/etc/options	Mon Mar 17 21:56:32 2014 +0100
+++ b/src/Tools/jEdit/etc/options	Mon Mar 17 23:16:26 2014 +0100
@@ -45,9 +45,6 @@
 public option jedit_completion_delay : real = 0.5
   -- "delay for completion popup (seconds)"
 
-public option jedit_completion_dismiss_delay : real = 0.0
-  -- "delay for dismissing obsolete completion popup (seconds)"
-
 public option jedit_completion_immediate : bool = false
   -- "insert unique completion immediately into buffer (if delay = 0)"
 
--- a/src/Tools/jEdit/src/completion_popup.scala	Mon Mar 17 21:56:32 2014 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala	Mon Mar 17 23:16:26 2014 +0100
@@ -112,7 +112,7 @@
       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
@@ -236,21 +236,35 @@
 
           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)
         }
       }
 
@@ -448,10 +462,10 @@
                   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 =>
           }
@@ -506,7 +520,7 @@
 
 
 class Completion_Popup private(
-  val active_range: Option[(Text.Range, () => Unit)],
+  val active_range: Option[Text.Range],
   layered: JLayeredPane,
   location: Point,
   font: Font,
@@ -524,7 +538,7 @@
 
   def complete(item: Completion.Item) { }
   def propagate(evt: KeyEvent) { }
-  def refocus() { }
+  def shutdown(focus: Boolean) { }
 
 
   /* list view */
@@ -568,7 +582,7 @@
 
   /* event handling */
 
-  private val inner_key_listener =
+  val inner_key_listener =
     JEdit_Lib.key_listener(
       key_pressed = (e: KeyEvent) =>
         {
@@ -639,27 +653,16 @@
     new Popup(layered, completion, screen.relative(layered, size), size)
   }
 
-  private def show_popup()
+  private def show_popup(focus: Boolean)
   {
     popup.show
-    list_view.requestFocus
+    if (focus) 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
-    }
-
   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
   }
 }