src/Tools/jEdit/src/plugin.scala

--- a/src/Tools/jEdit/src/plugin.scala	Wed Aug 28 09:12:50 2013 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Aug 28 09:36:05 2013 +0200
@@ -53,6 +53,16 @@
   lazy val editor = new JEdit_Editor
 
 
+  /* popups */
+
+  def dismissed_popups(view: View): Boolean =
+  {
+    val b1 = Completion_Popup.dismissed_view(view)
+    val b2 = Pretty_Tooltip.dismissed_all()
+    b1 || b2
+  }
+
+
   /* document model and view */
 
   def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
@@ -265,7 +275,7 @@
                 PIDE.init_view(buffer, text_area)
             }
             else {
-              Pretty_Tooltip.dismissed_all()
+              PIDE.dismissed_popups(text_area.getView)
               PIDE.exit_view(buffer, text_area)
             }
           }