explicit close button;

--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Sat Oct 06 16:03:41 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Sun Oct 07 15:05:11 2012 +0200
@@ -56,6 +56,8 @@
     legacy_pri -> load_icon("16x16/status/dialog-warning.png"),
     error_pri -> load_icon("16x16/status/dialog-error.png"))
 
+  val tooltip_close_icon = load_icon("16x16/actions/document-close.png")
+
 
   /* token markup -- text styles */
 

--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Oct 06 16:03:41 2012 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Sun Oct 07 15:05:11 2012 +0200
@@ -14,6 +14,9 @@
 import javax.swing.{SwingUtilities, JWindow, JPanel, JComponent, KeyStroke}
 import javax.swing.border.LineBorder
 
+import scala.swing.{FlowPanel, Label}
+import scala.swing.event.MouseClicked
+
 import org.gjt.sp.jedit.View
 import org.gjt.sp.jedit.textarea.TextArea
 
@@ -27,6 +30,9 @@
 {
   window =>
 
+  Swing_Thread.require()
+
+
   window.addWindowFocusListener(new WindowAdapter {
     override def windowLostFocus(e: WindowEvent) {
       if (!Window.getWindows.exists(w =>
@@ -56,6 +62,9 @@
   })
   window.getRootPane.setBorder(new LineBorder(Color.BLACK))
 
+
+  /* pretty text area */
+
   val pretty_text_area = new Pretty_Text_Area(view)
   pretty_text_area.getPainter.setBackground(rendering.tooltip_color)
   pretty_text_area.resize(
@@ -64,6 +73,22 @@
 
   window.add(pretty_text_area)
 
+
+  /* controls */
+
+  private val close = new Label {
+    icon = Isabelle_Rendering.tooltip_close_icon
+    tooltip = "Close tooltip window"
+    listenTo(mouse.clicks)
+    reactions += { case _: MouseClicked => window.dispose() }
+  }
+
+  private val controls = new FlowPanel(FlowPanel.Alignment.Right)(close)
+  window.add(controls.peer, BorderLayout.NORTH)
+
+
+  /* window geometry */
+
   {
     val font_metrics = pretty_text_area.getPainter.getFontMetrics
     val margin = Isabelle.options.int("jedit_tooltip_margin")  // FIXME via rendering?!
@@ -73,7 +98,7 @@
 
     val screen = Toolkit.getDefaultToolkit.getScreenSize
     val w = (font_metrics.charWidth(Pretty.spc) * margin) min (screen.width / 2)
-    val h = (font_metrics.getHeight * (lines + 2)) min (screen.height / 2)
+    val h = (font_metrics.getHeight * (lines + 3)) min (screen.height / 2)
     window.setSize(w, h)
   }