src/Tools/jEdit/src/jedit_lib.scala

 
 
 import isabelle._
 
 import java.awt.{Component, Container, Window, GraphicsEnvironment, Point, Rectangle}
+import java.awt.event.{KeyEvent, KeyListener}
 import javax.swing.{Icon, ImageIcon, JWindow}
 
 import scala.annotation.tailrec
 
 import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities}
+import org.gjt.sp.jedit.gui.KeyEventWorkaround
 import org.gjt.sp.jedit.buffer.JEditBuffer
 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter}
 
 
 object JEdit_Lib

   def load_image_icon(name: String): ImageIcon =
     load_icon(name) match {
       case icon: ImageIcon => icon
       case _ => error("Bad image icon: " + name)
     }
+
+
+  /* key listener */
+
+  def key_listener(
+    workaround: Boolean = true,
+    key_typed: KeyEvent => Unit = _ => (),
+    key_pressed: KeyEvent => Unit = _ => (),
+    key_released: KeyEvent => Unit = _ => ()): KeyListener =
+  {
+    def process_key_event(evt0: KeyEvent, handle: KeyEvent => Unit)
+    {
+      val evt = if (workaround) KeyEventWorkaround.processKeyEvent(evt0) else evt0
+      if (evt != null) handle(evt)
+    }
+
+    new KeyListener
+    {
+      def keyTyped(evt: KeyEvent) { process_key_event(evt, key_typed) }
+      def keyPressed(evt: KeyEvent) { process_key_event(evt, key_pressed) }
+      def keyReleased(evt: KeyEvent) { process_key_event(evt, key_released) }
+    }
+  }
 }