some key event handling in the manner of SideKickBindings, SideKickCompletionPopup;
authorwenzelm
Tue Aug 27 14:56:11 2013 +0200 (2013-08-27)
changeset 53228f6c6688961db
parent 53227 68cc55ceb7f6
child 53229 6ce8328d7912
some key event handling in the manner of SideKickBindings, SideKickCompletionPopup;
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/document_view.scala
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 13:07:31 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 14:56:11 2013 +0200
     1.3 @@ -11,13 +11,13 @@
     1.4  
     1.5  import java.awt.{Point, BorderLayout, Dimension}
     1.6  import java.awt.event.{KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent}
     1.7 -import javax.swing.{JPanel, JComponent, PopupFactory}
     1.8 +import javax.swing.{JPanel, JComponent, PopupFactory, SwingUtilities}
     1.9  
    1.10  import scala.swing.{ListView, ScrollPane}
    1.11  import scala.swing.event.MouseClicked
    1.12  
    1.13  import org.gjt.sp.jedit.View
    1.14 -import org.gjt.sp.jedit.gui.KeyEventWorkaround
    1.15 +import org.gjt.sp.jedit.textarea.JEditTextArea
    1.16  
    1.17  
    1.18  object Completion_Popup
    1.19 @@ -40,6 +40,31 @@
    1.20      completion.show_popup()
    1.21      completion
    1.22    }
    1.23 +
    1.24 +  def input_text_area(text_area: JEditTextArea, evt: KeyEvent)
    1.25 +  {
    1.26 +    Swing_Thread.require()
    1.27 +
    1.28 +    val buffer = text_area.getBuffer
    1.29 +    if (buffer.isEditable) {
    1.30 +      val painter = text_area.getPainter
    1.31 +      val caret = text_area.getCaretPosition
    1.32 +
    1.33 +      // FIXME
    1.34 +      def complete(item: Item) { }
    1.35 +      val token_length = 0
    1.36 +      val items: List[Item] = Nil
    1.37 +
    1.38 +      if (!items.isEmpty) {
    1.39 +        val location = text_area.offsetToXY(caret - token_length)
    1.40 +        if (location != null) {
    1.41 +          location.y = location.y + painter.getFontMetrics.getHeight
    1.42 +          SwingUtilities.convertPointToScreen(location, painter)
    1.43 +          apply(Some(text_area.getView), painter, location, items, complete _)
    1.44 +        }
    1.45 +      }
    1.46 +    }
    1.47 +  }
    1.48  }
    1.49  
    1.50  
    1.51 @@ -186,12 +211,18 @@
    1.52    def hide_popup()
    1.53    {
    1.54      opt_view match {
    1.55 -      case Some(view) if view.getKeyEventInterceptor == key_listener =>
    1.56 -        view.setKeyEventInterceptor(null)
    1.57 -      case _ =>
    1.58 +      case Some(view) =>
    1.59 +        if (view.getKeyEventInterceptor == key_listener)
    1.60 +          view.setKeyEventInterceptor(null)
    1.61 +        popup.hide
    1.62 +        view.getTextArea match {
    1.63 +          case null =>
    1.64 +          case text_area => text_area.requestFocus
    1.65 +        }
    1.66 +      case None =>
    1.67 +        popup.hide
    1.68 +        parent.requestFocus
    1.69      }
    1.70 -    popup.hide
    1.71 -    parent.requestFocus
    1.72    }
    1.73  }
    1.74  
     2.1 --- a/src/Tools/jEdit/src/document_view.scala	Tue Aug 27 13:07:31 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/document_view.scala	Tue Aug 27 14:56:11 2013 +0200
     2.3 @@ -151,6 +151,7 @@
     2.4  
     2.5    private val key_listener =
     2.6      JEdit_Lib.key_listener(
     2.7 +      key_typed = Completion_Popup.input_text_area(text_area, _),
     2.8        key_pressed = (evt: KeyEvent) =>
     2.9          {
    2.10            if (evt.getKeyCode == KeyEvent.VK_ESCAPE && Pretty_Tooltip.dismissed_all())