# HG changeset patch
# User wenzelm
# Date 1401440522 -7200
# Node ID a406e15c3cf7122ff93740ede493ff817d2ed71e
# Parent  3a928dffc37f33644042345ac4cdb0725a1bbfb2
make double-sure that old popup is dismissed, before replacing it;

diff -r 3a928dffc37f -r a406e15c3cf7 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Fri May 30 10:50:57 2014 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Fri May 30 11:02:02 2014 +0200
@@ -351,6 +351,7 @@
                 JEdit_Lib.invalidate_range(text_area, range)
               }
             }
+          dismissed()
           completion_popup = Some(completion)
           view.setKeyEventInterceptor(completion.inner_key_listener)
           JEdit_Lib.invalidate_range(text_area, range)
@@ -576,6 +577,7 @@
                   }
                   override def shutdown(focus: Boolean) { if (focus) text_field.requestFocus }
                 }
+              dismissed()
               completion_popup = Some(completion)
               completion.show_popup(true)