--- 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) {
--- 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)
}