--- a/src/Tools/jEdit/src/isabelle.scala Sun Mar 01 22:52:46 2020 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Mon Mar 02 13:43:39 2020 +0100
@@ -532,7 +532,7 @@
tip <- rendering.tooltip(caret_range, control)
loc0 <- Option(text_area.offsetToXY(caret_range.start))
} {
- val loc = new Point(loc0.x, loc0.y + painter.getLineHeight / 2)
+ val loc = new Point(loc0.x, loc0.y + painter.getLineHeight * 3 / 4)
val results = rendering.snapshot.command_results(tip.range)
Pretty_Tooltip(view, painter, loc, rendering, results, tip)
}