src/Tools/jEdit/src/pretty_text_area.scala

--- a/src/Tools/jEdit/src/pretty_text_area.scala	Wed Aug 28 09:12:50 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Wed Aug 28 09:36:05 2013 +0200
@@ -177,7 +177,7 @@
             evt.consume
 
           case KeyEvent.VK_ESCAPE =>
-            if (Pretty_Tooltip.dismissed_all()) evt.consume
+            if (PIDE.dismissed_popups(view)) evt.consume
 
           case _ =>
         }