--- 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)