src/Tools/jEdit/src/document_view.scala
changeset 53227 68cc55ceb7f6
parent 53226 9cf8e2263ca7
child 53228 f6c6688961db
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Tue Aug 27 12:35:32 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Tue Aug 27 13:07:31 2013 +0200
     1.3 @@ -151,10 +151,9 @@
     1.4  
     1.5    private val key_listener =
     1.6      JEdit_Lib.key_listener(
     1.7 -      workaround = false,
     1.8 -      key_typed = (evt: KeyEvent) =>
     1.9 +      key_pressed = (evt: KeyEvent) =>
    1.10          {
    1.11 -          if (evt.getKeyChar == 27 && Pretty_Tooltip.dismissed_all())
    1.12 +          if (evt.getKeyCode == KeyEvent.VK_ESCAPE && Pretty_Tooltip.dismissed_all())
    1.13              evt.consume
    1.14          }
    1.15      )