# HG changeset patch # User wenzelm # Date 1372678346 -7200 # Node ID 0f0f80e41581c2a44833406a49cb7f35bf80f30b # Parent d435febab3273cd5b468ae86a9fbe9ecef776cd1 tighten tooltip size; diff -r d435febab327 -r 0f0f80e41581 src/Tools/jEdit/src/pretty_tooltip.scala --- a/src/Tools/jEdit/src/pretty_tooltip.scala Mon Jul 01 12:01:24 2013 +0200 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala Mon Jul 01 13:32:26 2013 +0200 @@ -207,22 +207,34 @@ { val screen_bounds = JEdit_Lib.screen_bounds(screen_point) - val painter = pretty_text_area.getPainter - val metric = JEdit_Lib.pretty_metric(painter) - val margin = rendering.tooltip_margin * metric.average - val lines = - XML.traverse_text(Pretty.formatted(body, margin, metric))(0)( - (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length) + val (w, h) = + { + val painter = pretty_text_area.getPainter + val metric = JEdit_Lib.pretty_metric(painter) + val margin = rendering.tooltip_margin * metric.average + + val formatted = Pretty.formatted(body, margin, metric) + val lines = + XML.traverse_text(formatted)(0)( + (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length) + + val (deco_width, deco_height) = Pretty_Tooltip.decoration_size(tip) + val bounds = rendering.tooltip_bounds - val (deco_width, deco_height) = Pretty_Tooltip.decoration_size(tip) + val h1 = painter.getFontMetrics.getHeight * (lines + 1) + deco_height + val h2 = (screen_bounds.height * bounds).toInt + val h = h1 min h2 - val bounds = rendering.tooltip_bounds - val w = - ((metric.unit * (margin + metric.average)).round.toInt + deco_width) min - (screen_bounds.width * bounds).toInt - val h = - (painter.getFontMetrics.getHeight * (lines + 1) + deco_height) min - (screen_bounds.height * bounds).toInt + val margin1 = + if (h1 <= h2) + (0.0 /: split_lines(XML.content(formatted)))({ case (m, line) => m max metric(line) }) + else margin + val w = + ((metric.unit * (margin1 + metric.average)).round.toInt + deco_width) min + (screen_bounds.width * bounds).toInt + + (w, h) + } tip.setSize(new Dimension(w, h)) tip.setPreferredSize(new Dimension(w, h))