# HG changeset patch
# User wenzelm
# Date 1372683918 -7200
# Node ID 2dd4e4a368e3711e47ce3181a794d45b4dbccc82
# Parent  8188e528666260d5cf1525af4ed0b0d7d65e75ed
tuned signature;

diff -r 8188e5286662 -r 2dd4e4a368e3 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Mon Jul 01 14:56:10 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Mon Jul 01 15:05:18 2013 +0200
@@ -42,26 +42,24 @@
     rendering: Rendering,
     screen_point: Point,
     results: Command.Results,
-    info: Text.Info[XML.Body])
+    info: Text.Info[XML.Body]): Pretty_Tooltip =
   {
     Swing_Thread.require()
 
-    val same =
-      stack match {
-        case top :: _ => top.results == results && top.info == info
-        case Nil => false
-      }
-    if (!same) {
-      val (old, rest) =
-        JEdit_Lib.ancestors(parent).collectFirst({ case x: Pretty_Tooltip => x }) match {
-          case Some(tip) => hierarchy(tip).getOrElse((stack, Nil))
-          case None => (stack, Nil)
-        }
-      old.foreach(_.hide_popup)
-  
-      val tip = new Pretty_Tooltip(view, rendering, parent, screen_point, results, info)
-      stack = tip :: rest
-      tip.show_popup
+    stack match {
+      case top :: _ if top.results == results && top.info == info => top
+      case _ =>
+        val (old, rest) =
+          JEdit_Lib.ancestors(parent).collectFirst({ case x: Pretty_Tooltip => x }) match {
+            case Some(tip) => hierarchy(tip).getOrElse((stack, Nil))
+            case None => (stack, Nil)
+          }
+        old.foreach(_.hide_popup)
+
+        val tip = new Pretty_Tooltip(view, rendering, parent, screen_point, results, info)
+        stack = tip :: rest
+        tip.show_popup
+        tip
     }
   }