# HG changeset patch
# User wenzelm
# Date 1357317449 -3600
# Node ID 27478c11f63cf0e15b33b8148cae6083c70abf6f
# Parent  226a5b290c857d463bed3506c741f5311ac7875d
more elementary key handling: listen to low-level KEY_PRESSED events (without consuming);

diff -r 226a5b290c85 -r 27478c11f63c src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Fri Jan 04 17:33:55 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Fri Jan 04 17:37:29 2013 +0100
@@ -10,9 +10,8 @@
 
 import isabelle._
 
-import java.awt.{Color, Font, FontMetrics, Toolkit}
-import java.awt.event.{ActionListener, ActionEvent, KeyEvent}
-import javax.swing.{KeyStroke, JComponent}
+import java.awt.{Color, Font, FontMetrics, Toolkit, Window}
+import java.awt.event.{KeyEvent, KeyAdapter}
 
 import org.gjt.sp.jedit.{jEdit, View, Registers}
 import org.gjt.sp.jedit.textarea.{AntiAlias, JEditEmbeddedTextArea}
@@ -159,22 +158,24 @@
   }
 
 
-  /* keyboard actions */
+  /* key handling */
 
-  private val action_listener = new ActionListener {
-    def actionPerformed(e: ActionEvent) {
-      e.getActionCommand match {
-        case "copy" => Registers.copy(text_area, '$')
+  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, '$')
+        case KeyEvent.VK_ESCAPE =>
+          Window.getWindows foreach {
+            case c: Pretty_Tooltip => c.dispose
+            case _ =>
+          }
         case _ =>
       }
     }
-  }
-
-  registerKeyboardAction(action_listener, "copy",
-    KeyStroke.getKeyStroke(KeyEvent.VK_COPY, 0), JComponent.WHEN_FOCUSED)
-  registerKeyboardAction(action_listener, "copy",
-    KeyStroke.getKeyStroke(KeyEvent.VK_C,
-      Toolkit.getDefaultToolkit().getMenuShortcutKeyMask()), JComponent.WHEN_FOCUSED)
+  })
 
 
   /* init */
diff -r 226a5b290c85 -r 27478c11f63c src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Jan 04 17:33:55 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Jan 04 17:37:29 2013 +0100
@@ -10,8 +10,8 @@
 import isabelle._
 
 import java.awt.{Color, Point, BorderLayout, Window, Dimension}
-import java.awt.event.{ActionListener, ActionEvent, KeyEvent, WindowEvent, WindowAdapter}
-import javax.swing.{SwingUtilities, JDialog, JPanel, JComponent, KeyStroke}
+import java.awt.event.{WindowEvent, WindowAdapter}
+import javax.swing.{SwingUtilities, JDialog, JPanel, JComponent}
 import javax.swing.border.LineBorder
 
 import scala.swing.{FlowPanel, Label}
@@ -37,7 +37,6 @@
 
   window.setUndecorated(true)
   window.setFocusableWindowState(true)
-  window.setAutoRequestFocus(true)
 
   window.addWindowFocusListener(new WindowAdapter {
     override def windowLostFocus(e: WindowEvent) {
@@ -47,24 +46,8 @@
     }
   })
 
-  private val action_listener = new ActionListener {
-    def actionPerformed(e: ActionEvent) {
-      e.getActionCommand match {
-        case "close_all" =>
-          Window.getWindows foreach {
-            case c: Pretty_Tooltip => c.dispose
-            case _ =>
-          }
-        case _ =>
-      }
-    }
-  }
-
   window.setContentPane(new JPanel(new BorderLayout) {
     setBackground(rendering.tooltip_color)
-    registerKeyboardAction(action_listener, "close_all",
-      KeyStroke.getKeyStroke(KeyEvent.VK_ESCAPE, 0), JComponent.WHEN_FOCUSED)
-
     override def getFocusTraversalKeysEnabled(): Boolean = false
   })
   window.getRootPane.setBorder(new LineBorder(Color.BLACK))
@@ -77,9 +60,6 @@
     Rendering.font_size("jedit_tooltip_font_scale").round)
   pretty_text_area.update(rendering.snapshot, results, body)
 
-  pretty_text_area.registerKeyboardAction(action_listener, "close_all",
-    KeyStroke.getKeyStroke(KeyEvent.VK_ESCAPE, 0), JComponent.WHEN_FOCUSED)
-
   window.add(pretty_text_area)
 
 
@@ -136,6 +116,7 @@
   }
 
   window.setVisible(true)
+  pretty_text_area.requestFocus
   pretty_text_area.refresh()
 }