src/Tools/jEdit/src/document_view.scala
changeset 53274 1760c01f1c78
parent 53272 0dfd78ff7696
child 53780 ef62204a126b
--- a/src/Tools/jEdit/src/document_view.scala	Thu Aug 29 10:24:43 2013 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Thu Aug 29 12:38:33 2013 +0200
@@ -149,19 +149,13 @@
 
   /* 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) =>
         {
           if (evt.getKeyCode == KeyEvent.VK_ESCAPE && PIDE.dismissed_popups(text_area.getView))
             evt.consume
-        },
-      key_typed = completion_popup.input _
+        }
     )