tuned;
authorwenzelm
Wed Aug 28 10:35:12 2013 +0200 (2013-08-28)
changeset 53245301b69957af7
parent 53244 ec6011bf2362
child 53246 8d34caf5bf82
tuned;
src/Tools/jEdit/src/document_view.scala
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Wed Aug 28 09:36:05 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Wed Aug 28 10:35:12 2013 +0200
     1.3 @@ -151,12 +151,12 @@
     1.4  
     1.5    private val key_listener =
     1.6      JEdit_Lib.key_listener(
     1.7 -      key_typed = Completion_Popup.Text_Area.input(text_area, PIDE.get_recent_syntax, _),
     1.8        key_pressed = (evt: KeyEvent) =>
     1.9          {
    1.10            if (evt.getKeyCode == KeyEvent.VK_ESCAPE && PIDE.dismissed_popups(text_area.getView))
    1.11              evt.consume
    1.12 -        }
    1.13 +        },
    1.14 +      key_typed = Completion_Popup.Text_Area.input(text_area, PIDE.get_recent_syntax, _)
    1.15      )
    1.16  
    1.17