# HG changeset patch
# User wenzelm
# Date 1355417193 -3600
# Node ID 51408dde956f9415211b5d590410d92fc3cc6504
# Parent  6f41f1646617c7b1a30ca8d1407f5fe31c473cf1
include command results in tooltip as well;

diff -r 6f41f1646617 -r 51408dde956f src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Thu Dec 13 17:29:23 2012 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Thu Dec 13 17:46:33 2012 +0100
@@ -264,6 +264,14 @@
         }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
 
 
+  def command_results(range: Text.Range): Command.Results =
+  {
+    val results =
+      snapshot.select_markup[Command.Results](range, None, command_state =>
+        { case _ => command_state.results }).map(_.info)
+    (Command.empty_results /: results)(_ ++ _)
+  }
+
   def tooltip_message(range: Text.Range): XML.Body =
   {
     val msgs =
diff -r 6f41f1646617 -r 51408dde956f src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Thu Dec 13 17:29:23 2012 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Thu Dec 13 17:46:33 2012 +0100
@@ -204,14 +204,14 @@
           JEdit_Lib.pixel_range(text_area, x, y) match {
             case None =>
             case Some(range) =>
-              // FIXME cumulate results!?
               val tip =
                 if (control) rendering.tooltip(range)
                 else rendering.tooltip_message(range)
               if (!tip.isEmpty) {
                 val painter = text_area.getPainter
                 val y1 = y + painter.getFontMetrics.getHeight / 2
-                new Pretty_Tooltip(view, painter, rendering, x, y1, Command.empty_results, tip)
+                val results = rendering.command_results(range)
+                new Pretty_Tooltip(view, painter, rendering, x, y1, results, tip)
               }
           }
         }