# HG changeset patch
# User wenzelm
# Date 1377633635 -7200
# Node ID 1b6a44859549438bde90eadfb12af8cf80c9f5eb
# Parent  ea4abbbe1702b66fe7f9f216ea486d241d2e342d
register single instance within root, in order to get rid of old popup as user continues typing;

diff -r ea4abbbe1702 -r 1b6a44859549 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 20:58:53 2013 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 22:00:35 2013 +0200
@@ -22,10 +22,29 @@
 
 object Completion_Popup
 {
+  /* items */
+
   private sealed case class Item(original: String, replacement: String, description: String)
   { override def toString: String = description }
 
-  private def complete_item(text_area: JEditTextArea, item: Item)
+
+  /* register single instance within root */
+
+  private def register(root: JComponent, completion: Completion_Popup)
+  {
+    Swing_Thread.require()
+
+    root.getClientProperty(Completion_Popup) match {
+      case old_completion: Completion_Popup => old_completion.hide_popup
+      case _ =>
+    }
+    root.putClientProperty(Completion_Popup, completion)
+  }
+
+
+  /* jEdit text area operations */
+
+  private def complete_text_area(text_area: JEditTextArea, item: Item)
   {
     Swing_Thread.require()
 
@@ -48,16 +67,16 @@
   {
     Swing_Thread.require()
 
+    val view = text_area.getView
+    val root = view.getRootPane
     val buffer = text_area.getBuffer
+    val painter = text_area.getPainter
+
     if (buffer.isEditable) {
       get_syntax match {
-        case None =>
         case Some(syntax) =>
-          val view = text_area.getView
-          val painter = text_area.getPainter
-
           val caret = text_area.getCaretPosition
-          val completion =
+          val result =
           {
             val line = buffer.getLineOfOffset(caret)
             val start = buffer.getLineStartOffset(line)
@@ -74,8 +93,7 @@
                 else Some((word, ds.map(s => Item(word, s, s))))
             }
           }
-          completion match {
-            case None =>
+          result match {
             case Some((original, items)) =>
               val popup_font =
                 painter.getFont.deriveFont(
@@ -86,15 +104,25 @@
               if (location != null) {
                 location.y = location.y + painter.getFontMetrics.getHeight
                 SwingUtilities.convertPointToScreen(location, painter)
-                new Completion_Popup(view.getRootPane, popup_font, location, items) {
-                  override def complete(item: Item) { complete_item(text_area, item) }
-                  override def propagate(evt: KeyEvent) { JEdit_Lib.propagate_key(view, evt) }
-                  override def refocus() { text_area.requestFocus }
-                }
+
+                val completion =
+                  new Completion_Popup(root, popup_font, location, items) {
+                    override def complete(item: Item) { complete_text_area(text_area, item) }
+                    override def propagate(e: KeyEvent) {
+                      JEdit_Lib.propagate_key(view, e)
+                      if (!e.isConsumed) input_text_area(text_area, get_syntax, e)
+                    }
+                    override def refocus() { text_area.requestFocus }
+                  }
+                register(root, completion)
               }
+              else register(root, null)
+            case None => register(root, null)
           }
+        case None => register(root, null)
       }
     }
+    else register(root, null)
   }
 }