enable jEdit KeyEventWorkaround uniformly;
authorwenzelm
Tue Aug 27 22:23:40 2013 +0200 (2013-08-27)
changeset 532376bfe54791591
parent 53236 837a6ef61fe9
child 53238 01ef0a103fc9
enable jEdit KeyEventWorkaround uniformly;
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/jedit_lib.scala
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 22:20:11 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 22:23:40 2013 +0200
     1.3 @@ -186,7 +186,6 @@
     1.4  
     1.5    private val key_listener =
     1.6      JEdit_Lib.key_listener(
     1.7 -      workaround = false,
     1.8        key_pressed = (e: KeyEvent) =>
     1.9          {
    1.10            if (!e.isConsumed) {
     2.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Tue Aug 27 22:20:11 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Tue Aug 27 22:23:40 2013 +0200
     2.3 @@ -307,14 +307,13 @@
     2.4    }
     2.5  
     2.6    def key_listener(
     2.7 -    workaround: Boolean = true,
     2.8      key_typed: KeyEvent => Unit = _ => (),
     2.9      key_pressed: KeyEvent => Unit = _ => (),
    2.10      key_released: KeyEvent => Unit = _ => ()): KeyListener =
    2.11    {
    2.12      def process_key_event(evt0: KeyEvent, handle: KeyEvent => Unit)
    2.13      {
    2.14 -      val evt = if (workaround) KeyEventWorkaround.processKeyEvent(evt0) else evt0
    2.15 +      val evt = KeyEventWorkaround.processKeyEvent(evt0)
    2.16        if (evt != null) handle(evt)
    2.17      }
    2.18