src/Tools/jEdit/src/document_view.scala
changeset 53272 0dfd78ff7696
parent 53245 301b69957af7
child 53274 1760c01f1c78
--- a/src/Tools/jEdit/src/document_view.scala	Thu Aug 29 09:16:03 2013 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Thu Aug 29 10:01:59 2013 +0200
@@ -149,6 +149,11 @@
 
   /* key listener */
 
+  private val completion_popup =
+    Completion_Popup.Text_Area(text_area, PIDE.get_recent_syntax)
+
+  def dismissed_popups(): Boolean = completion_popup.dismissed()
+
   private val key_listener =
     JEdit_Lib.key_listener(
       key_pressed = (evt: KeyEvent) =>
@@ -156,7 +161,7 @@
           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, _)
+      key_typed = completion_popup.input _
     )