# HG changeset patch
# User wenzelm
# Date 1353599753 -3600
# Node ID 4f2b5b2a9ad58360efc1a195dfb5500b9eda8942
# Parent  2585c81d840af42ff4ea9e15d43752013717d575
more precise tooltip window size;

diff -r 2585c81d840a -r 4f2b5b2a9ad5 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Thu Nov 22 15:22:27 2012 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Thu Nov 22 16:55:53 2012 +0100
@@ -9,7 +9,7 @@
 
 import isabelle._
 
-import java.awt.{Toolkit, Color, Point, BorderLayout, Window}
+import java.awt.{Toolkit, Color, Point, BorderLayout, Window, Dimension}
 import java.awt.event.{ActionListener, ActionEvent, KeyEvent, WindowEvent, WindowAdapter}
 import javax.swing.{SwingUtilities, JWindow, JPanel, JComponent, KeyStroke}
 import javax.swing.border.LineBorder
@@ -73,7 +73,7 @@
   pretty_text_area.update(rendering.snapshot, body)
 
   pretty_text_area.registerKeyboardAction(action_listener, "close_all",
-      KeyStroke.getKeyStroke(KeyEvent.VK_ESCAPE, 0), JComponent.WHEN_FOCUSED)
+    KeyStroke.getKeyStroke(KeyEvent.VK_ESCAPE, 0), JComponent.WHEN_FOCUSED)
 
   window.add(pretty_text_area)
 
@@ -107,14 +107,14 @@
   {
     val font_metrics = pretty_text_area.getPainter.getFontMetrics
     val margin = Isabelle.options.int("jedit_tooltip_margin")  // FIXME via rendering?!
-    val lines =  // FIXME avoid redundant formatting
+    val lines =
       XML.traverse_text(Pretty.formatted(body, margin, Pretty.font_metric(font_metrics)))(0)(
         (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
 
     val screen = Toolkit.getDefaultToolkit.getScreenSize
-    val w = (font_metrics.charWidth(Pretty.spc) * margin) min (screen.width / 2)
-    val h = (font_metrics.getHeight * (lines + 2) + 25) min (screen.height / 2)
-    window.setSize(w, h)
+    val w = (font_metrics.charWidth(Pretty.spc) * (margin + 2)) min (screen.width / 2)
+    val h = (font_metrics.getHeight * (lines + 2)) min (screen.height / 2)
+    pretty_text_area.setPreferredSize(new Dimension(w, h))
   }
 
   {
@@ -128,6 +128,7 @@
   }
 
   window.setVisible(true)
-  pretty_text_area.refresh()  // FIXME avoid redundant formatting
+  window.pack
+  pretty_text_area.refresh()
 }