src/Tools/jEdit/src/document_view.scala
changeset 52548 a1a8248a4677
parent 52479 bb516d01d259
child 52759 a20631db9c8a
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Sun Jul 07 17:52:13 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Sun Jul 07 18:04:46 2013 +0200
     1.3 @@ -152,7 +152,8 @@
     1.4    private val key_listener = new KeyAdapter {
     1.5      override def keyTyped(evt: KeyEvent)
     1.6      {
     1.7 -      if (evt.getKeyChar == 27) Pretty_Tooltip.dismiss_all()
     1.8 +      if (evt.getKeyChar == 27 && Pretty_Tooltip.dismissed_all())
     1.9 +        evt.consume
    1.10      }
    1.11    }
    1.12