# HG changeset patch
# User wenzelm
# Date 1399409275 -7200
# Node ID 3020f6bbd1190e9c53b6ea8d1a58756f331157e0
# Parent  7de69b35bdaf1b33154bed0db31788b186bd0bae
clarified GUI events, e.g. relevant for insert via completion;

diff -r 7de69b35bdaf -r 3020f6bbd119 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Tue May 06 22:01:43 2014 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Tue May 06 22:47:55 2014 +0200
@@ -13,6 +13,7 @@
 import java.awt.{Color, Font, FontMetrics, Toolkit, Window}
 import java.awt.event.KeyEvent
 import javax.swing.JTextField
+import javax.swing.event.{DocumentListener, DocumentEvent}
 
 import java.util.concurrent.{Future => JFuture}
 
@@ -191,11 +192,11 @@
           Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
             search_action(this)
           }
-        override def processKeyEvent(evt: KeyEvent)
-        {
-          super.processKeyEvent(evt)
-          input_delay.invoke()
-        }
+        getDocument.addDocumentListener(new DocumentListener {
+          def changedUpdate(e: DocumentEvent) { input_delay.invoke() }
+          def insertUpdate(e: DocumentEvent) { input_delay.invoke() }
+          def removeUpdate(e: DocumentEvent) { input_delay.invoke() }
+        })
         setColumns(20)
         setToolTipText(search_label.tooltip)
         setFont(GUI.imitate_font(Font_Info.main_family(), getFont, 1.2))