more careful refocus operation: do not reset focus if it was already lost (relevant when activating a different GUI component, for example);
authorwenzelm
Tue Aug 27 20:58:53 2013 +0200 (2013-08-27 ago)
changeset 53234ea4abbbe1702
parent 53233 4b422e5d64fd
child 53235 1b6a44859549
more careful refocus operation: do not reset focus if it was already lost (relevant when activating a different GUI component, for example);
src/Tools/jEdit/src/completion_popup.scala
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 20:45:02 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 20:58:53 2013 +0200
     1.3 @@ -89,7 +89,7 @@
     1.4                  new Completion_Popup(view.getRootPane, popup_font, location, items) {
     1.5                    override def complete(item: Item) { complete_item(text_area, item) }
     1.6                    override def propagate(evt: KeyEvent) { JEdit_Lib.propagate_key(view, evt) }
     1.7 -                  override def hidden() { text_area.requestFocus }
     1.8 +                  override def refocus() { text_area.requestFocus }
     1.9                  }
    1.10                }
    1.11            }
    1.12 @@ -115,7 +115,7 @@
    1.13  
    1.14    def complete(item: Completion_Popup.Item) { }
    1.15    def propagate(evt: KeyEvent) { }
    1.16 -  def hidden() { }
    1.17 +  def refocus() { }
    1.18  
    1.19  
    1.20    /* list view */
    1.21 @@ -240,8 +240,9 @@
    1.22  
    1.23    private def hide_popup()
    1.24    {
    1.25 +    val had_focus = list_view.peer.isFocusOwner
    1.26      popup.hide
    1.27 -    hidden()
    1.28 +    if (had_focus) refocus()
    1.29    }
    1.30  
    1.31    popup.show