src/Tools/jEdit/src/pretty_tooltip.scala

 
 
 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}
 import scala.swing.event.MouseClicked
 

   Swing_Thread.require()
 
 
   window.setUndecorated(true)
   window.setFocusableWindowState(true)
-  window.setAutoRequestFocus(true)
 
   window.addWindowFocusListener(new WindowAdapter {
     override def windowLostFocus(e: WindowEvent) {
       if (!Window.getWindows.exists(w =>
             w.isDisplayable && JEdit_Lib.ancestors(w).exists(_ == window)))
         window.dispose()
     }
   })
 
-  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))
 
 

 
   val pretty_text_area = new Pretty_Text_Area(view, Some(rendering.tooltip_color))
   pretty_text_area.resize(Rendering.font_family(),
     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)
 
 
   /* controls */

     val y = screen_point.y min (screen_bounds.y + screen_bounds.height - window.getHeight)
     window.setLocation(x, y)
   }
 
   window.setVisible(true)
+  pretty_text_area.requestFocus
   pretty_text_area.refresh()
 }