--- a/src/Tools/jEdit/src/pretty_tooltip.scala Sat Mar 16 10:50:23 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Sat Mar 16 12:46:22 2013 +0100
@@ -97,16 +97,27 @@
val screen_bounds = JEdit_Lib.screen_bounds(screen_point)
{
- val fm = pretty_text_area.getPainter.getFontMetrics
+ val painter = pretty_text_area.getPainter
+ val fm = painter.getFontMetrics
val margin = rendering.tooltip_margin
val lines =
XML.traverse_text(Pretty.formatted(body, margin, Pretty.font_metric(fm)))(0)(
(n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
+ window.setPreferredSize(new Dimension(100, 100))
+ window.pack
+ val deco_width = window.getWidth - painter.getWidth
+ val deco_height = window.getHeight - painter.getHeight
+
val bounds = rendering.tooltip_bounds
- val w = (Pretty.char_width_int(fm) * (margin + 2)) min (screen_bounds.width * bounds).toInt
- val h = (fm.getHeight * (lines + 2)) min (screen_bounds.height * bounds).toInt
- pretty_text_area.setPreferredSize(new Dimension(w, h))
+ val w =
+ ((Pretty.char_width(fm) * (margin + 1)).round.toInt + deco_width) min
+ (screen_bounds.width * bounds).toInt
+ val h =
+ (fm.getHeight * (lines + 1) + deco_height) min
+ (screen_bounds.height * bounds).toInt
+
+ window.setPreferredSize(new Dimension(w, h))
window.pack
val x = screen_point.x min (screen_bounds.x + screen_bounds.width - window.getWidth)