equal
deleted
inserted
replaced
102 val margin = rendering.tooltip_margin |
102 val margin = rendering.tooltip_margin |
103 val lines = |
103 val lines = |
104 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)( |
105 (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length) |
105 (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length) |
106 |
106 |
|
107 window.setSize(new Dimension(100, 100)) |
107 window.setPreferredSize(new Dimension(100, 100)) |
108 window.setPreferredSize(new Dimension(100, 100)) |
108 window.pack |
109 window.pack |
109 val deco_width = window.getWidth - painter.getWidth |
110 val deco_width = window.getWidth - painter.getWidth |
110 val deco_height = window.getHeight - painter.getHeight |
111 val deco_height = window.getHeight - painter.getHeight |
111 |
112 |
115 (screen_bounds.width * bounds).toInt |
116 (screen_bounds.width * bounds).toInt |
116 val h = |
117 val h = |
117 (fm.getHeight * (lines + 1) + deco_height) min |
118 (fm.getHeight * (lines + 1) + deco_height) min |
118 (screen_bounds.height * bounds).toInt |
119 (screen_bounds.height * bounds).toInt |
119 |
120 |
|
121 window.setSize(new Dimension(w, h)) |
120 window.setPreferredSize(new Dimension(w, h)) |
122 window.setPreferredSize(new Dimension(w, h)) |
121 window.pack |
123 window.pack |
|
124 window.revalidate |
122 |
125 |
123 val x = screen_point.x min (screen_bounds.x + screen_bounds.width - window.getWidth) |
126 val x = screen_point.x min (screen_bounds.x + screen_bounds.width - window.getWidth) |
124 val y = screen_point.y min (screen_bounds.y + screen_bounds.height - window.getHeight) |
127 val y = screen_point.y min (screen_bounds.y + screen_bounds.height - window.getHeight) |
125 window.setLocation(x, y) |
128 window.setLocation(x, y) |
126 } |
129 } |