src/Tools/jEdit/src/document_view.scala
changeset 53274 1760c01f1c78
parent 53272 0dfd78ff7696
child 53780 ef62204a126b
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Thu Aug 29 10:24:43 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Thu Aug 29 12:38:33 2013 +0200
     1.3 @@ -149,19 +149,13 @@
     1.4  
     1.5    /* key listener */
     1.6  
     1.7 -  private val completion_popup =
     1.8 -    Completion_Popup.Text_Area(text_area, PIDE.get_recent_syntax)
     1.9 -
    1.10 -  def dismissed_popups(): Boolean = completion_popup.dismissed()
    1.11 -
    1.12    private val key_listener =
    1.13      JEdit_Lib.key_listener(
    1.14        key_pressed = (evt: KeyEvent) =>
    1.15          {
    1.16            if (evt.getKeyCode == KeyEvent.VK_ESCAPE && PIDE.dismissed_popups(text_area.getView))
    1.17              evt.consume
    1.18 -        },
    1.19 -      key_typed = completion_popup.input _
    1.20 +        }
    1.21      )
    1.22  
    1.23