equal
deleted
inserted
replaced
530 doc_view <- Document_View.get(text_area) |
530 doc_view <- Document_View.get(text_area) |
531 rendering = doc_view.get_rendering() |
531 rendering = doc_view.get_rendering() |
532 tip <- rendering.tooltip(caret_range, control) |
532 tip <- rendering.tooltip(caret_range, control) |
533 loc0 <- Option(text_area.offsetToXY(caret_range.start)) |
533 loc0 <- Option(text_area.offsetToXY(caret_range.start)) |
534 } { |
534 } { |
535 val loc = new Point(loc0.x, loc0.y + painter.getLineHeight / 2) |
535 val loc = new Point(loc0.x, loc0.y + painter.getLineHeight * 3 / 4) |
536 val results = rendering.snapshot.command_results(tip.range) |
536 val results = rendering.snapshot.command_results(tip.range) |
537 Pretty_Tooltip(view, painter, loc, rendering, results, tip) |
537 Pretty_Tooltip(view, painter, loc, rendering, results, tip) |
538 } |
538 } |
539 } |
539 } |
540 |
540 |