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