# HG changeset patch
# User wenzelm
# Date 1377608171 -7200
# Node ID f6c6688961db2960ba06c640103334ef78da55ed
# Parent  68cc55ceb7f6f013b5a275f30cdb705fcbe19504
some key event handling in the manner of SideKickBindings, SideKickCompletionPopup;

diff -r 68cc55ceb7f6 -r f6c6688961db src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 13:07:31 2013 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 14:56:11 2013 +0200
@@ -11,13 +11,13 @@
 
 import java.awt.{Point, BorderLayout, Dimension}
 import java.awt.event.{KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent}
-import javax.swing.{JPanel, JComponent, PopupFactory}
+import javax.swing.{JPanel, JComponent, PopupFactory, SwingUtilities}
 
 import scala.swing.{ListView, ScrollPane}
 import scala.swing.event.MouseClicked
 
 import org.gjt.sp.jedit.View
-import org.gjt.sp.jedit.gui.KeyEventWorkaround
+import org.gjt.sp.jedit.textarea.JEditTextArea
 
 
 object Completion_Popup
@@ -40,6 +40,31 @@
     completion.show_popup()
     completion
   }
+
+  def input_text_area(text_area: JEditTextArea, evt: KeyEvent)
+  {
+    Swing_Thread.require()
+
+    val buffer = text_area.getBuffer
+    if (buffer.isEditable) {
+      val painter = text_area.getPainter
+      val caret = text_area.getCaretPosition
+
+      // FIXME
+      def complete(item: Item) { }
+      val token_length = 0
+      val items: List[Item] = Nil
+
+      if (!items.isEmpty) {
+        val location = text_area.offsetToXY(caret - token_length)
+        if (location != null) {
+          location.y = location.y + painter.getFontMetrics.getHeight
+          SwingUtilities.convertPointToScreen(location, painter)
+          apply(Some(text_area.getView), painter, location, items, complete _)
+        }
+      }
+    }
+  }
 }
 
 
@@ -186,12 +211,18 @@
   def hide_popup()
   {
     opt_view match {
-      case Some(view) if view.getKeyEventInterceptor == key_listener =>
-        view.setKeyEventInterceptor(null)
-      case _ =>
+      case Some(view) =>
+        if (view.getKeyEventInterceptor == key_listener)
+          view.setKeyEventInterceptor(null)
+        popup.hide
+        view.getTextArea match {
+          case null =>
+          case text_area => text_area.requestFocus
+        }
+      case None =>
+        popup.hide
+        parent.requestFocus
     }
-    popup.hide
-    parent.requestFocus
   }
 }
 
diff -r 68cc55ceb7f6 -r f6c6688961db src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Tue Aug 27 13:07:31 2013 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Tue Aug 27 14:56:11 2013 +0200
@@ -151,6 +151,7 @@
 
   private val key_listener =
     JEdit_Lib.key_listener(
+      key_typed = Completion_Popup.input_text_area(text_area, _),
       key_pressed = (evt: KeyEvent) =>
         {
           if (evt.getKeyCode == KeyEvent.VK_ESCAPE && Pretty_Tooltip.dismissed_all())