src/Tools/jEdit/src/document_view.scala
changeset 53226 9cf8e2263ca7
parent 53179 336cd976698c
child 53227 68cc55ceb7f6
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Mon Aug 26 23:39:53 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Tue Aug 27 12:35:32 2013 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4  import java.lang.System
     1.5  import java.text.BreakIterator
     1.6  import java.awt.{Color, Graphics2D, Point}
     1.7 -import java.awt.event.{KeyEvent, KeyAdapter}
     1.8 +import java.awt.event.KeyEvent
     1.9  import javax.swing.event.{CaretListener, CaretEvent}
    1.10  
    1.11  import org.gjt.sp.jedit.{jEdit, Debug}
    1.12 @@ -149,13 +149,15 @@
    1.13  
    1.14    /* key listener */
    1.15  
    1.16 -  private val key_listener = new KeyAdapter {
    1.17 -    override def keyTyped(evt: KeyEvent)
    1.18 -    {
    1.19 -      if (evt.getKeyChar == 27 && Pretty_Tooltip.dismissed_all())
    1.20 -        evt.consume
    1.21 -    }
    1.22 -  }
    1.23 +  private val key_listener =
    1.24 +    JEdit_Lib.key_listener(
    1.25 +      workaround = false,
    1.26 +      key_typed = (evt: KeyEvent) =>
    1.27 +        {
    1.28 +          if (evt.getKeyChar == 27 && Pretty_Tooltip.dismissed_all())
    1.29 +            evt.consume
    1.30 +        }
    1.31 +    )
    1.32  
    1.33  
    1.34    /* caret handling */