src/Tools/jEdit/src/plugin.scala

--- a/src/Tools/jEdit/src/plugin.scala	Thu Aug 29 09:16:03 2013 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Thu Aug 29 10:01:59 2013 +0200
@@ -57,9 +57,16 @@
 
   def dismissed_popups(view: View): Boolean =
   {
-    val b1 = Completion_Popup.dismissed(view.getLayeredPane)
-    val b2 = Pretty_Tooltip.dismissed_all()
-    b1 || b2
+    var dismissed = false
+
+    for {
+      text_area <- JEdit_Lib.jedit_text_areas(view)
+      doc_view <- document_view(text_area)
+    } { if (doc_view.dismissed_popups()) dismissed = true }
+
+    if (Pretty_Tooltip.dismissed_all()) dismissed = true
+
+    dismissed
   }