# HG changeset patch # User wenzelm # Date 1377599732 -7200 # Node ID 9cf8e2263ca74046146ed81bde15ec6e62d0e513 # Parent bae01293f4dd2bcb0d04a1399e14eee08c211388 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround; diff -r bae01293f4dd -r 9cf8e2263ca7 src/Tools/jEdit/src/completion_popup.scala --- a/src/Tools/jEdit/src/completion_popup.scala Mon Aug 26 23:39:53 2013 +0200 +++ b/src/Tools/jEdit/src/completion_popup.scala Tue Aug 27 12:35:32 2013 +0200 @@ -10,13 +10,14 @@ import isabelle._ import java.awt.{Point, BorderLayout, Dimension} -import java.awt.event.{KeyEvent, KeyAdapter, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent} +import java.awt.event.{KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent} import javax.swing.{JPanel, JComponent, PopupFactory} import scala.swing.{ListView, ScrollPane} import scala.swing.event.MouseClicked import org.gjt.sp.jedit.View +import org.gjt.sp.jedit.gui.KeyEventWorkaround object Completion_Popup @@ -92,49 +93,50 @@ /* event handling */ - private val key_handler = new KeyAdapter { - override def keyPressed(e: KeyEvent) - { - if (!e.isConsumed) { - e.getKeyCode match { - case KeyEvent.VK_TAB => - if (complete_selected()) e.consume - hide_popup() - case KeyEvent.VK_ESCAPE => - hide_popup() - e.consume - case KeyEvent.VK_UP => move_items(-1); e.consume - case KeyEvent.VK_DOWN => move_items(1); e.consume - case KeyEvent.VK_PAGE_UP => move_pages(-1); e.consume - case KeyEvent.VK_PAGE_DOWN => move_pages(1); e.consume - case _ => - if (e.isActionKey || e.isAltDown || e.isMetaDown || e.isControlDown) - hide_popup() + private val key_listener = + JEdit_Lib.key_listener( + workaround = false, + key_pressed = (e: KeyEvent) => + { + if (!e.isConsumed) { + e.getKeyCode match { + case KeyEvent.VK_TAB => + if (complete_selected()) e.consume + hide_popup() + case KeyEvent.VK_ESCAPE => + hide_popup() + e.consume + case KeyEvent.VK_UP => move_items(-1); e.consume + case KeyEvent.VK_DOWN => move_items(1); e.consume + case KeyEvent.VK_PAGE_UP => move_pages(-1); e.consume + case KeyEvent.VK_PAGE_DOWN => move_pages(1); e.consume + case _ => + if (e.isActionKey || e.isAltDown || e.isMetaDown || e.isControlDown) + hide_popup() + } + } + if (!e.isConsumed) pass_to_view(e) + }, + key_typed = (e: KeyEvent) => + { + if (!e.isConsumed) pass_to_view(e) } - } - if (!e.isConsumed) pass_to_view(e) - } - - override def keyTyped(e: KeyEvent) - { - if (!e.isConsumed) pass_to_view(e) - } - } + ) private def pass_to_view(e: KeyEvent) { opt_view match { - case Some(view) if view.getKeyEventInterceptor == key_handler => + case Some(view) if view.getKeyEventInterceptor == key_listener => try { view.setKeyEventInterceptor(null) view.getInputHandler().processKeyEvent(e, View.ACTION_BAR, false) } - finally { view.setKeyEventInterceptor(key_handler) } + finally { view.setKeyEventInterceptor(key_listener) } case _ => } } - list_view.peer.addKeyListener(key_handler) + list_view.peer.addKeyListener(key_listener) list_view.peer.addMouseListener(new MouseAdapter { override def mouseClicked(e: MouseEvent) { @@ -176,7 +178,7 @@ def show_popup() { - opt_view.foreach(view => view.setKeyEventInterceptor(key_handler)) + opt_view.foreach(view => view.setKeyEventInterceptor(key_listener)) popup.show list_view.requestFocus } @@ -184,7 +186,7 @@ def hide_popup() { opt_view match { - case Some(view) if view.getKeyEventInterceptor == key_handler => + case Some(view) if view.getKeyEventInterceptor == key_listener => view.setKeyEventInterceptor(null) case _ => } diff -r bae01293f4dd -r 9cf8e2263ca7 src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Mon Aug 26 23:39:53 2013 +0200 +++ b/src/Tools/jEdit/src/document_view.scala Tue Aug 27 12:35:32 2013 +0200 @@ -17,7 +17,7 @@ import java.lang.System import java.text.BreakIterator import java.awt.{Color, Graphics2D, Point} -import java.awt.event.{KeyEvent, KeyAdapter} +import java.awt.event.KeyEvent import javax.swing.event.{CaretListener, CaretEvent} import org.gjt.sp.jedit.{jEdit, Debug} @@ -149,13 +149,15 @@ /* key listener */ - private val key_listener = new KeyAdapter { - override def keyTyped(evt: KeyEvent) - { - if (evt.getKeyChar == 27 && Pretty_Tooltip.dismissed_all()) - evt.consume - } - } + private val key_listener = + JEdit_Lib.key_listener( + workaround = false, + key_typed = (evt: KeyEvent) => + { + if (evt.getKeyChar == 27 && Pretty_Tooltip.dismissed_all()) + evt.consume + } + ) /* caret handling */ diff -r bae01293f4dd -r 9cf8e2263ca7 src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala Mon Aug 26 23:39:53 2013 +0200 +++ b/src/Tools/jEdit/src/jedit_lib.scala Tue Aug 27 12:35:32 2013 +0200 @@ -10,11 +10,13 @@ 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} @@ -300,5 +302,28 @@ 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) } + } + } } diff -r bae01293f4dd -r 9cf8e2263ca7 src/Tools/jEdit/src/pretty_text_area.scala --- a/src/Tools/jEdit/src/pretty_text_area.scala Mon Aug 26 23:39:53 2013 +0200 +++ b/src/Tools/jEdit/src/pretty_text_area.scala Tue Aug 27 12:35:32 2013 +0200 @@ -11,7 +11,7 @@ import isabelle._ import java.awt.{Color, Font, FontMetrics, Toolkit, Window} -import java.awt.event.{KeyEvent, KeyAdapter} +import java.awt.event.KeyEvent import org.gjt.sp.jedit.{jEdit, View, Registers} import org.gjt.sp.jedit.textarea.{AntiAlias, JEditEmbeddedTextArea} @@ -162,33 +162,33 @@ /* key handling */ - addKeyListener(new KeyAdapter { - override def keyPressed(evt: KeyEvent) - { - evt.getKeyCode match { - case KeyEvent.VK_C - if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 => - Registers.copy(text_area, '$') + addKeyListener(JEdit_Lib.key_listener( + workaround = false, + key_pressed = (evt: KeyEvent) => + { + evt.getKeyCode match { + case KeyEvent.VK_C + if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 => + Registers.copy(text_area, '$') + evt.consume + case KeyEvent.VK_A + if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 => + text_area.selectAll + evt.consume + case _ => + } + if (propagate_keys && !evt.isConsumed) + view.getInputHandler.processKeyEvent(evt, View.ACTION_BAR, false) + }, + key_typed = (evt: KeyEvent) => + { + if (evt.getKeyChar == 27 && Pretty_Tooltip.dismissed_all()) evt.consume - case KeyEvent.VK_A - if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 => - text_area.selectAll - evt.consume - case _ => + if (propagate_keys && !evt.isConsumed) + view.getInputHandler.processKeyEvent(evt, View.ACTION_BAR, false) } - if (propagate_keys && !evt.isConsumed) - view.getInputHandler.processKeyEvent(evt, View.ACTION_BAR, false) - } - - override def keyTyped(evt: KeyEvent) - { - if (evt.getKeyChar == 27 && Pretty_Tooltip.dismissed_all()) - evt.consume - - if (propagate_keys && !evt.isConsumed) - view.getInputHandler.processKeyEvent(evt, View.ACTION_BAR, false) - } - }) + ) + ) /* init */