src/Tools/jEdit/src/completion_popup.scala
changeset 54376 3eb84b6b0353
parent 53987 16a0cd5293d9
child 54377 750561986828
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Thu Nov 07 19:35:57 2013 +0100
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Fri Nov 08 15:10:16 2013 +0100
     1.3 @@ -490,9 +490,8 @@
     1.4  
     1.5    private def hide_popup()
     1.6    {
     1.7 -    val had_focus = list_view.peer.isFocusOwner
     1.8 +    if (list_view.peer.isFocusOwner) refocus()
     1.9      popup.hide
    1.10 -    if (had_focus) refocus()
    1.11    }
    1.12  }
    1.13