src/Tools/jEdit/src/completion_popup.scala
changeset 53226 9cf8e2263ca7
parent 53023 f127e949389f
child 53228 f6c6688961db
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Mon Aug 26 23:39:53 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 12:35:32 2013 +0200
     1.3 @@ -10,13 +10,14 @@
     1.4  import isabelle._
     1.5  
     1.6  import java.awt.{Point, BorderLayout, Dimension}
     1.7 -import java.awt.event.{KeyEvent, KeyAdapter, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent}
     1.8 +import java.awt.event.{KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent}
     1.9  import javax.swing.{JPanel, JComponent, PopupFactory}
    1.10  
    1.11  import scala.swing.{ListView, ScrollPane}
    1.12  import scala.swing.event.MouseClicked
    1.13  
    1.14  import org.gjt.sp.jedit.View
    1.15 +import org.gjt.sp.jedit.gui.KeyEventWorkaround
    1.16  
    1.17  
    1.18  object Completion_Popup
    1.19 @@ -92,49 +93,50 @@
    1.20  
    1.21    /* event handling */
    1.22  
    1.23 -  private val key_handler = new KeyAdapter {
    1.24 -    override def keyPressed(e: KeyEvent)
    1.25 -    {
    1.26 -      if (!e.isConsumed) {
    1.27 -        e.getKeyCode match {
    1.28 -          case KeyEvent.VK_TAB =>
    1.29 -            if (complete_selected()) e.consume
    1.30 -            hide_popup()
    1.31 -          case KeyEvent.VK_ESCAPE =>
    1.32 -            hide_popup()
    1.33 -            e.consume
    1.34 -          case KeyEvent.VK_UP => move_items(-1); e.consume
    1.35 -          case KeyEvent.VK_DOWN => move_items(1); e.consume
    1.36 -          case KeyEvent.VK_PAGE_UP => move_pages(-1); e.consume
    1.37 -          case KeyEvent.VK_PAGE_DOWN => move_pages(1); e.consume
    1.38 -          case _ =>
    1.39 -            if (e.isActionKey || e.isAltDown || e.isMetaDown || e.isControlDown)
    1.40 -              hide_popup()
    1.41 +  private val key_listener =
    1.42 +    JEdit_Lib.key_listener(
    1.43 +      workaround = false,
    1.44 +      key_pressed = (e: KeyEvent) =>
    1.45 +        {
    1.46 +          if (!e.isConsumed) {
    1.47 +            e.getKeyCode match {
    1.48 +              case KeyEvent.VK_TAB =>
    1.49 +                if (complete_selected()) e.consume
    1.50 +                hide_popup()
    1.51 +              case KeyEvent.VK_ESCAPE =>
    1.52 +                hide_popup()
    1.53 +                e.consume
    1.54 +              case KeyEvent.VK_UP => move_items(-1); e.consume
    1.55 +              case KeyEvent.VK_DOWN => move_items(1); e.consume
    1.56 +              case KeyEvent.VK_PAGE_UP => move_pages(-1); e.consume
    1.57 +              case KeyEvent.VK_PAGE_DOWN => move_pages(1); e.consume
    1.58 +              case _ =>
    1.59 +                if (e.isActionKey || e.isAltDown || e.isMetaDown || e.isControlDown)
    1.60 +                  hide_popup()
    1.61 +            }
    1.62 +          }
    1.63 +          if (!e.isConsumed) pass_to_view(e)
    1.64 +        },
    1.65 +      key_typed = (e: KeyEvent) =>
    1.66 +        {
    1.67 +          if (!e.isConsumed) pass_to_view(e)
    1.68          }
    1.69 -      }
    1.70 -      if (!e.isConsumed) pass_to_view(e)
    1.71 -    }
    1.72 -
    1.73 -    override def keyTyped(e: KeyEvent)
    1.74 -    {
    1.75 -      if (!e.isConsumed) pass_to_view(e)
    1.76 -    }
    1.77 -  }
    1.78 +    )
    1.79  
    1.80    private def pass_to_view(e: KeyEvent)
    1.81    {
    1.82      opt_view match {
    1.83 -      case Some(view) if view.getKeyEventInterceptor == key_handler =>
    1.84 +      case Some(view) if view.getKeyEventInterceptor == key_listener =>
    1.85          try {
    1.86            view.setKeyEventInterceptor(null)
    1.87            view.getInputHandler().processKeyEvent(e, View.ACTION_BAR, false)
    1.88          }
    1.89 -        finally { view.setKeyEventInterceptor(key_handler) }
    1.90 +        finally { view.setKeyEventInterceptor(key_listener) }
    1.91        case _ =>
    1.92      }
    1.93    }
    1.94  
    1.95 -  list_view.peer.addKeyListener(key_handler)
    1.96 +  list_view.peer.addKeyListener(key_listener)
    1.97  
    1.98    list_view.peer.addMouseListener(new MouseAdapter {
    1.99      override def mouseClicked(e: MouseEvent) {
   1.100 @@ -176,7 +178,7 @@
   1.101  
   1.102    def show_popup()
   1.103    {
   1.104 -    opt_view.foreach(view => view.setKeyEventInterceptor(key_handler))
   1.105 +    opt_view.foreach(view => view.setKeyEventInterceptor(key_listener))
   1.106      popup.show
   1.107      list_view.requestFocus
   1.108    }
   1.109 @@ -184,7 +186,7 @@
   1.110    def hide_popup()
   1.111    {
   1.112      opt_view match {
   1.113 -      case Some(view) if view.getKeyEventInterceptor == key_handler =>
   1.114 +      case Some(view) if view.getKeyEventInterceptor == key_listener =>
   1.115          view.setKeyEventInterceptor(null)
   1.116        case _ =>
   1.117      }