95 val screen_point = new Point(mouse_x, mouse_y) |
95 val screen_point = new Point(mouse_x, mouse_y) |
96 SwingUtilities.convertPointToScreen(screen_point, parent) |
96 SwingUtilities.convertPointToScreen(screen_point, parent) |
97 val screen_bounds = JEdit_Lib.screen_bounds(screen_point) |
97 val screen_bounds = JEdit_Lib.screen_bounds(screen_point) |
98 |
98 |
99 { |
99 { |
100 val fm = pretty_text_area.getPainter.getFontMetrics |
100 val painter = pretty_text_area.getPainter |
|
101 val fm = painter.getFontMetrics |
101 val margin = rendering.tooltip_margin |
102 val margin = rendering.tooltip_margin |
102 val lines = |
103 val lines = |
103 XML.traverse_text(Pretty.formatted(body, margin, Pretty.font_metric(fm)))(0)( |
104 XML.traverse_text(Pretty.formatted(body, margin, Pretty.font_metric(fm)))(0)( |
104 (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length) |
105 (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length) |
105 |
106 |
|
107 window.setPreferredSize(new Dimension(100, 100)) |
|
108 window.pack |
|
109 val deco_width = window.getWidth - painter.getWidth |
|
110 val deco_height = window.getHeight - painter.getHeight |
|
111 |
106 val bounds = rendering.tooltip_bounds |
112 val bounds = rendering.tooltip_bounds |
107 val w = (Pretty.char_width_int(fm) * (margin + 2)) min (screen_bounds.width * bounds).toInt |
113 val w = |
108 val h = (fm.getHeight * (lines + 2)) min (screen_bounds.height * bounds).toInt |
114 ((Pretty.char_width(fm) * (margin + 1)).round.toInt + deco_width) min |
109 pretty_text_area.setPreferredSize(new Dimension(w, h)) |
115 (screen_bounds.width * bounds).toInt |
|
116 val h = |
|
117 (fm.getHeight * (lines + 1) + deco_height) min |
|
118 (screen_bounds.height * bounds).toInt |
|
119 |
|
120 window.setPreferredSize(new Dimension(w, h)) |
110 window.pack |
121 window.pack |
111 |
122 |
112 val x = screen_point.x min (screen_bounds.x + screen_bounds.width - window.getWidth) |
123 val x = screen_point.x min (screen_bounds.x + screen_bounds.width - window.getWidth) |
113 val y = screen_point.y min (screen_bounds.y + screen_bounds.height - window.getHeight) |
124 val y = screen_point.y min (screen_bounds.y + screen_bounds.height - window.getHeight) |
114 window.setLocation(x, y) |
125 window.setLocation(x, y) |