make double-sure that old popup is dismissed, before replacing it;
authorwenzelm
Fri May 30 11:02:02 2014 +0200 (2014-05-30 ago)
changeset 57127a406e15c3cf7
parent 57126 3a928dffc37f
child 57128 4874411752fe
make double-sure that old popup is dismissed, before replacing it;
src/Tools/jEdit/src/completion_popup.scala
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Fri May 30 10:50:57 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Fri May 30 11:02:02 2014 +0200
     1.3 @@ -351,6 +351,7 @@
     1.4                  JEdit_Lib.invalidate_range(text_area, range)
     1.5                }
     1.6              }
     1.7 +          dismissed()
     1.8            completion_popup = Some(completion)
     1.9            view.setKeyEventInterceptor(completion.inner_key_listener)
    1.10            JEdit_Lib.invalidate_range(text_area, range)
    1.11 @@ -576,6 +577,7 @@
    1.12                    }
    1.13                    override def shutdown(focus: Boolean) { if (focus) text_field.requestFocus }
    1.14                  }
    1.15 +              dismissed()
    1.16                completion_popup = Some(completion)
    1.17                completion.show_popup(true)
    1.18