src/Tools/jEdit/src/pretty_text_area.scala

--- a/src/Tools/jEdit/src/pretty_text_area.scala	Mon Mar 18 11:04:59 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Mon Mar 18 11:29:50 2013 +0100
@@ -170,7 +170,7 @@
           Registers.copy(text_area, '$')
           evt.consume
         case KeyEvent.VK_ESCAPE =>
-          Pretty_Tooltip.windows().foreach(_.dispose)
+          Pretty_Tooltip.windows().foreach(_.dismiss)
           evt.consume
         case _ =>
       }