src/Tools/jEdit/src/document_view.scala
changeset 53242 142f4fff4e40
parent 53233 4b422e5d64fd
child 53244 ec6011bf2362
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Wed Aug 28 00:18:50 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Wed Aug 28 09:08:36 2013 +0200
     1.3 @@ -151,7 +151,7 @@
     1.4  
     1.5    private val key_listener =
     1.6      JEdit_Lib.key_listener(
     1.7 -      key_typed = Completion_Popup.input_text_area(text_area, PIDE.get_recent_syntax, _),
     1.8 +      key_typed = Completion_Popup.Text_Area.input(text_area, PIDE.get_recent_syntax, _),
     1.9        key_pressed = (evt: KeyEvent) =>
    1.10          {
    1.11            if (evt.getKeyCode == KeyEvent.VK_ESCAPE && Pretty_Tooltip.dismissed_all())