diff -r 301b69957af7 -r 8d34caf5bf82 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Wed Aug 28 10:35:12 2013 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Aug 28 15:14:58 2013 +0200
@@ -57,7 +57,7 @@
 
   def dismissed_popups(view: View): Boolean =
   {
-    val b1 = Completion_Popup.dismissed_view(view)
+    val b1 = Completion_Popup.dismissed(view.getLayeredPane)
     val b2 = Pretty_Tooltip.dismissed_all()
     b1 || b2
   }