src/Tools/jEdit/src/document_view.scala
changeset 53274 1760c01f1c78
parent 53272 0dfd78ff7696
child 53780 ef62204a126b
equal deleted inserted replaced
53273:473ea1ed7503 53274:1760c01f1c78
   147   }
   147   }
   148 
   148 
   149 
   149 
   150   /* key listener */
   150   /* key listener */
   151 
   151 
   152   private val completion_popup =
       
   153     Completion_Popup.Text_Area(text_area, PIDE.get_recent_syntax)
       
   154 
       
   155   def dismissed_popups(): Boolean = completion_popup.dismissed()
       
   156 
       
   157   private val key_listener =
   152   private val key_listener =
   158     JEdit_Lib.key_listener(
   153     JEdit_Lib.key_listener(
   159       key_pressed = (evt: KeyEvent) =>
   154       key_pressed = (evt: KeyEvent) =>
   160         {
   155         {
   161           if (evt.getKeyCode == KeyEvent.VK_ESCAPE && PIDE.dismissed_popups(text_area.getView))
   156           if (evt.getKeyCode == KeyEvent.VK_ESCAPE && PIDE.dismissed_popups(text_area.getView))
   162             evt.consume
   157             evt.consume
   163         },
   158         }
   164       key_typed = completion_popup.input _
       
   165     )
   159     )
   166 
   160 
   167 
   161 
   168   /* caret handling */
   162   /* caret handling */
   169 
   163