src/Tools/jEdit/src/document_view.scala
changeset 53233 4b422e5d64fd
parent 53228 f6c6688961db
child 53242 142f4fff4e40
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Tue Aug 27 17:17:20 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Tue Aug 27 20:45:02 2013 +0200
     1.3 @@ -151,7 +151,7 @@
     1.4  
     1.5    private val key_listener =
     1.6      JEdit_Lib.key_listener(
     1.7 -      key_typed = Completion_Popup.input_text_area(text_area, _),
     1.8 +      key_typed = Completion_Popup.input_text_area(text_area, PIDE.get_recent_syntax, _),
     1.9        key_pressed = (evt: KeyEvent) =>
    1.10          {
    1.11            if (evt.getKeyCode == KeyEvent.VK_ESCAPE && Pretty_Tooltip.dismissed_all())