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);
--- 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
--- 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)