tuned;
authorwenzelm
Wed, 28 Aug 2013 10:35:12 +0200
changeset 53245 301b69957af7
parent 53244 ec6011bf2362
child 53246 8d34caf5bf82
tuned;
src/Tools/jEdit/src/document_view.scala
--- 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, _)
     )