src/Tools/jEdit/src/document_view.scala
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())