# HG changeset patch # User wenzelm # Date 1349619991 -7200 # Node ID 74f36dab2b626d663ad7a8db70c046db133861b9 # Parent 2fe56b60069842f1c06c715ae71718e11f673edd close tooltips more thoroughly; diff -r 2fe56b600698 -r 74f36dab2b62 src/Tools/jEdit/src/pretty_tooltip.scala --- a/src/Tools/jEdit/src/pretty_tooltip.scala Sun Oct 07 16:15:31 2012 +0200 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala Sun Oct 07 16:26:31 2012 +0200 @@ -41,21 +41,21 @@ } }) - window.setContentPane(new JPanel(new BorderLayout) { - private val action_listener = new ActionListener { - def actionPerformed(e: ActionEvent) { - e.getActionCommand match { - case "close" => - window.dispose() - JEdit_Lib.ancestors(window) foreach { - case c: Pretty_Tooltip => c.dispose - case _ => - } - case _ => - } + 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 _ => } } - registerKeyboardAction(action_listener, "close", + } + + window.setContentPane(new JPanel(new BorderLayout) { + registerKeyboardAction(action_listener, "close_all", KeyStroke.getKeyStroke(KeyEvent.VK_ESCAPE, 0), JComponent.WHEN_FOCUSED) override def getFocusTraversalKeysEnabled(): Boolean = false @@ -71,6 +71,9 @@ Isabelle.font_family(), Isabelle.font_size("jedit_tooltip_font_scale").round) pretty_text_area.update(rendering.snapshot, body) + pretty_text_area.registerKeyboardAction(action_listener, "close_all", + KeyStroke.getKeyStroke(KeyEvent.VK_ESCAPE, 0), JComponent.WHEN_FOCUSED) + window.add(pretty_text_area)