--- a/src/Tools/jEdit/src/document_view.scala Wed Aug 28 09:36:05 2013 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Wed Aug 28 10:35:12 2013 +0200
@@ -151,12 +151,12 @@
private val key_listener =
JEdit_Lib.key_listener(
- key_typed = Completion_Popup.Text_Area.input(text_area, PIDE.get_recent_syntax, _),
key_pressed = (evt: KeyEvent) =>
{
if (evt.getKeyCode == KeyEvent.VK_ESCAPE && PIDE.dismissed_popups(text_area.getView))
evt.consume
- }
+ },
+ key_typed = Completion_Popup.Text_Area.input(text_area, PIDE.get_recent_syntax, _)
)