--- 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()
}