src/Tools/jEdit/src/plugin.scala

     if (current_session.recent_syntax == Outer_Syntax.empty) None
     else Some(current_session.recent_syntax)
   }
 
   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)

                 msg.getWhat == EditPaneUpdate.CREATED) {
               if (PIDE.session.is_ready)
                 PIDE.init_view(buffer, text_area)
             }
             else {
-              Pretty_Tooltip.dismissed_all()
+              PIDE.dismissed_popups(text_area.getView)
               PIDE.exit_view(buffer, text_area)
             }
           }
 
         case msg: PropertiesChanged =>