# HG changeset patch
# User wenzelm
# Date 1583153019 -3600
# Node ID f2a79950748e77f16024b772aa0934b7bec2bd6c
# Parent  df7494f1438864c222da50c4b8b049865f42c0ee
tuned GUI;

diff -r df7494f14388 -r f2a79950748e src/Tools/jEdit/src/isabelle.scala
--- 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)
     }