# HG changeset patch
# User wenzelm
# Date 1377678912 -7200
# Node ID 301b69957af7bc84613f374e85ce300dca994646
# Parent  ec6011bf23629a26071483a895737b77764c2a67
tuned;

diff -r ec6011bf2362 -r 301b69957af7 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, _)
     )