src/Tools/jEdit/src/document_view.scala
changeset 53244 ec6011bf2362
parent 53242 142f4fff4e40
child 53245 301b69957af7
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Wed Aug 28 09:12:50 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Wed Aug 28 09:36:05 2013 +0200
     1.3 @@ -154,7 +154,7 @@
     1.4        key_typed = Completion_Popup.Text_Area.input(text_area, PIDE.get_recent_syntax, _),
     1.5        key_pressed = (evt: KeyEvent) =>
     1.6          {
     1.7 -          if (evt.getKeyCode == KeyEvent.VK_ESCAPE && Pretty_Tooltip.dismissed_all())
     1.8 +          if (evt.getKeyCode == KeyEvent.VK_ESCAPE && PIDE.dismissed_popups(text_area.getView))
     1.9              evt.consume
    1.10          }
    1.11      )