# HG changeset patch
# User wenzelm
# Date 1363434382 -3600
# Node ID b10b64679c5b13b94f09e2401173542f6d2f9716
# Parent  c22bd20b0d63f1ee99181de55ab52d61449eb67c
more precise tooltip window size (NB: dimensions are known after layout pack, before making content visible);
more precise margin width based on fractional Pretty.char_width (avoid multiplication of rounding errors);
early initialization of gutter to get proper text area painter size (see also 2585c81d840a);

diff -r c22bd20b0d63 -r b10b64679c5b src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sat Mar 16 10:50:23 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sat Mar 16 12:46:22 2013 +0100
@@ -93,23 +93,22 @@
     }
     getPainter.setFoldLineStyle(fold_line_style)
 
+    getGutter.setForeground(jEdit.getColorProperty("view.gutter.fgColor"))
+    getGutter.setBackground(jEdit.getColorProperty("view.gutter.bgColor"))
+    background.map(bg => { getPainter.setBackground(bg); getGutter.setBackground(bg) })
+    getGutter.setHighlightedForeground(jEdit.getColorProperty("view.gutter.highlightColor"))
+    getGutter.setFoldColor(jEdit.getColorProperty("view.gutter.foldColor"))
+    getGutter.setFont(jEdit.getFontProperty("view.gutter.font"))
+    getGutter.setBorder(0,
+      jEdit.getColorProperty("view.gutter.focusBorderColor"),
+      jEdit.getColorProperty("view.gutter.noFocusBorderColor"),
+      getPainter.getBackground)
+    getGutter.setFoldPainter(getFoldPainter)
+    getGutter.setGutterEnabled(jEdit.getBooleanProperty("view.gutter.enabled"))
+
     if (getWidth > 0) {
-      getGutter.setForeground(jEdit.getColorProperty("view.gutter.fgColor"))
-      getGutter.setBackground(jEdit.getColorProperty("view.gutter.bgColor"))
-      background.map(bg => { getPainter.setBackground(bg); getGutter.setBackground(bg) })
-      getGutter.setHighlightedForeground(jEdit.getColorProperty("view.gutter.highlightColor"))
-      getGutter.setFoldColor(jEdit.getColorProperty("view.gutter.foldColor"))
-      getGutter.setFont(jEdit.getFontProperty("view.gutter.font"))
-      getGutter.setBorder(0,
-        jEdit.getColorProperty("view.gutter.focusBorderColor"),
-        jEdit.getColorProperty("view.gutter.noFocusBorderColor"),
-        getPainter.getBackground)
-      getGutter.setFoldPainter(getFoldPainter)
-
-      getGutter.setGutterEnabled(jEdit.getBooleanProperty("view.gutter.enabled"))
-
       val fm = getPainter.getFontMetrics
-      val margin = ((getWidth - getGutter.getWidth) / (Pretty.char_width_int(fm) max 1) - 2) max 20
+      val margin = (getPainter.getWidth / (Pretty.char_width_int(fm) max 1)) max 20
 
       val base_snapshot = current_base_snapshot
       val base_results = current_base_results
diff -r c22bd20b0d63 -r b10b64679c5b src/Tools/jEdit/src/pretty_tooltip.scala
--- 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)