--- 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 _ =>
}
--- 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 */
--- 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) }
+ }
+ }
}
--- 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 */