src/Tools/jEdit/src/completion_popup.scala
changeset 56197 416f7a00e4cb
parent 56177 bfa9dfb722de
child 56325 ffbfc92e6508
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Mon Mar 17 21:56:32 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Mon Mar 17 23:16:26 2014 +0100
     1.3 @@ -112,7 +112,7 @@
     1.4        completion_popup match {
     1.5          case Some(completion) =>
     1.6            completion.active_range match {
     1.7 -            case Some((range, _)) if completion.isDisplayable => Some(range)
     1.8 +            case Some(range) if completion.isDisplayable => Some(range)
     1.9              case _ => None
    1.10            }
    1.11          case None => None
    1.12 @@ -236,21 +236,35 @@
    1.13  
    1.14            val items = result.items.map(new Item(_))
    1.15            val completion =
    1.16 -            new Completion_Popup(Some((range, invalidate _)), layered, loc2, font, items)
    1.17 +            new Completion_Popup(Some(range), layered, loc2, font, items)
    1.18              {
    1.19                override def complete(item: Completion.Item) {
    1.20                  PIDE.completion_history.update(item)
    1.21                  insert(item)
    1.22                }
    1.23                override def propagate(evt: KeyEvent) {
    1.24 -                JEdit_Lib.propagate_key(view, evt)
    1.25 +                if (view.getKeyEventInterceptor == inner_key_listener) {
    1.26 +                  try {
    1.27 +                    view.setKeyEventInterceptor(null)
    1.28 +                    JEdit_Lib.propagate_key(view, evt)
    1.29 +                  }
    1.30 +                  finally {
    1.31 +                    if (isDisplayable) view.setKeyEventInterceptor(inner_key_listener)
    1.32 +                  }
    1.33 +                }
    1.34                  if (evt.getID == KeyEvent.KEY_TYPED) input(evt)
    1.35                }
    1.36 -              override def refocus() { text_area.requestFocus }
    1.37 +              override def shutdown(focus: Boolean) {
    1.38 +                if (view.getKeyEventInterceptor == inner_key_listener)
    1.39 +                  view.setKeyEventInterceptor(null)
    1.40 +                if (focus) text_area.requestFocus
    1.41 +                invalidate()
    1.42 +              }
    1.43              }
    1.44            completion_popup = Some(completion)
    1.45 +          view.setKeyEventInterceptor(completion.inner_key_listener)
    1.46            invalidate()
    1.47 -          completion.show_popup()
    1.48 +          completion.show_popup(false)
    1.49          }
    1.50        }
    1.51  
    1.52 @@ -448,10 +462,10 @@
    1.53                    override def propagate(evt: KeyEvent) {
    1.54                      if (!evt.isConsumed) text_field.processKeyEvent(evt)
    1.55                    }
    1.56 -                  override def refocus() { text_field.requestFocus }
    1.57 +                  override def shutdown(focus: Boolean) { if (focus) text_field.requestFocus }
    1.58                  }
    1.59                completion_popup = Some(completion)
    1.60 -              completion.show_popup()
    1.61 +              completion.show_popup(true)
    1.62  
    1.63              case None =>
    1.64            }
    1.65 @@ -506,7 +520,7 @@
    1.66  
    1.67  
    1.68  class Completion_Popup private(
    1.69 -  val active_range: Option[(Text.Range, () => Unit)],
    1.70 +  val active_range: Option[Text.Range],
    1.71    layered: JLayeredPane,
    1.72    location: Point,
    1.73    font: Font,
    1.74 @@ -524,7 +538,7 @@
    1.75  
    1.76    def complete(item: Completion.Item) { }
    1.77    def propagate(evt: KeyEvent) { }
    1.78 -  def refocus() { }
    1.79 +  def shutdown(focus: Boolean) { }
    1.80  
    1.81  
    1.82    /* list view */
    1.83 @@ -568,7 +582,7 @@
    1.84  
    1.85    /* event handling */
    1.86  
    1.87 -  private val inner_key_listener =
    1.88 +  val inner_key_listener =
    1.89      JEdit_Lib.key_listener(
    1.90        key_pressed = (e: KeyEvent) =>
    1.91          {
    1.92 @@ -639,27 +653,16 @@
    1.93      new Popup(layered, completion, screen.relative(layered, size), size)
    1.94    }
    1.95  
    1.96 -  private def show_popup()
    1.97 +  private def show_popup(focus: Boolean)
    1.98    {
    1.99      popup.show
   1.100 -    list_view.requestFocus
   1.101 +    if (focus) list_view.requestFocus
   1.102    }
   1.103  
   1.104 -  private val hide_popup_delay =
   1.105 -    Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_dismiss_delay")) {
   1.106 -      active_range match { case Some((_, invalidate)) => invalidate() case _ => }
   1.107 -      popup.hide
   1.108 -    }
   1.109 -
   1.110    private def hide_popup()
   1.111    {
   1.112 -    if (list_view.peer.isFocusOwner) refocus()
   1.113 -
   1.114 -    if (PIDE.options.seconds("jedit_completion_dismiss_delay").is_zero) {
   1.115 -      active_range match { case Some((_, invalidate)) => invalidate() case _ => }
   1.116 -      popup.hide
   1.117 -    }
   1.118 -    else hide_popup_delay.invoke()
   1.119 +    shutdown(list_view.peer.isFocusOwner)
   1.120 +    popup.hide
   1.121    }
   1.122  }
   1.123