# HG changeset patch
# User wenzelm
# Date 1377635020 -7200
# Node ID 6bfe54791591f5760da85cb16c841b81152efec5
# Parent  837a6ef61fe942b518fb4cdd3f5f197a1cd25912
enable jEdit KeyEventWorkaround uniformly;

diff -r 837a6ef61fe9 -r 6bfe54791591 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 22:20:11 2013 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 22:23:40 2013 +0200
@@ -186,7 +186,6 @@
 
   private val key_listener =
     JEdit_Lib.key_listener(
-      workaround = false,
       key_pressed = (e: KeyEvent) =>
         {
           if (!e.isConsumed) {
diff -r 837a6ef61fe9 -r 6bfe54791591 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Tue Aug 27 22:20:11 2013 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Tue Aug 27 22:23:40 2013 +0200
@@ -307,14 +307,13 @@
   }
 
   def key_listener(
-    workaround: Boolean = true,
     key_typed: KeyEvent => Unit = _ => (),
     key_pressed: KeyEvent => Unit = _ => (),
     key_released: KeyEvent => Unit = _ => ()): KeyListener =
   {
     def process_key_event(evt0: KeyEvent, handle: KeyEvent => Unit)
     {
-      val evt = if (workaround) KeyEventWorkaround.processKeyEvent(evt0) else evt0
+      val evt = KeyEventWorkaround.processKeyEvent(evt0)
       if (evt != null) handle(evt)
     }