# HG changeset patch
# User wenzelm
# Date 1397049562 -7200
# Node ID 46b29bb1c627974662c61d8b2b6c76634263ca53
# Parent  0b9334adcf05abc5c61f145a0c1de270d6e58d8c
clarifed results range;

diff -r 0b9334adcf05 -r 46b29bb1c627 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Wed Apr 09 15:03:07 2014 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Wed Apr 09 15:19:22 2014 +0200
@@ -247,7 +247,7 @@
                         case Some(tip) =>
                           val painter = text_area.getPainter
                           val loc = new Point(x, y + painter.getFontMetrics.getHeight / 2)
-                          val results = rendering.command_results(range)
+                          val results = rendering.command_results(tip.range)
                           Pretty_Tooltip(view, painter, loc, rendering, results, tip)
                       }
                   }