src/Tools/jEdit/src/pretty_text_area.scala

--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sat Jun 29 12:57:04 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sat Jun 29 16:53:19 2013 +0200
@@ -171,7 +171,7 @@
           Registers.copy(text_area, '$')
           evt.consume
         case KeyEvent.VK_ESCAPE =>
-          Pretty_Tooltip.windows().foreach(_.dismiss)
+          Pretty_Tooltip.dismiss_all()
           evt.consume
         case _ =>
       }