equal
deleted
inserted
replaced
203 val offset = text_area.xyToOffset(x, y) |
203 val offset = text_area.xyToOffset(x, y) |
204 val range = Text.Range(offset, offset + 1) |
204 val range = Text.Range(offset, offset + 1) |
205 val tip = |
205 val tip = |
206 if (control) rendering.tooltip(range) |
206 if (control) rendering.tooltip(range) |
207 else rendering.tooltip_message(range) |
207 else rendering.tooltip_message(range) |
208 if (!tip.isEmpty) new Pretty_Tooltip(view, text_area, rendering, x, y, tip) |
208 if (!tip.isEmpty) { |
|
209 val painter = text_area.getPainter |
|
210 val y1 = y + painter.getFontMetrics.getHeight / 2 |
|
211 new Pretty_Tooltip(view, painter, rendering, x, y1, tip) |
|
212 } |
209 } |
213 } |
210 null |
214 null |
211 } |
215 } |
212 } |
216 } |
213 } |
217 } |