# HG changeset patch
# User wenzelm
# Date 1582990739 -3600
# Node ID 5d62f797e40cb59a852aeb9826baa1a15d69c22d
# Parent  633a8d52fef2b29b62261a50549d018941ad6c4e
tuned signature;

diff -r 633a8d52fef2 -r 5d62f797e40c src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Sat Feb 29 16:30:30 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Sat Feb 29 16:38:59 2020 +0100
@@ -297,11 +297,11 @@
   def tooltip_margin: Int = options.int("jedit_tooltip_margin")
   override def timing_threshold: Double = options.real("jedit_timing_threshold")
 
-  def tooltip(range: Text.Range): Option[Text.Info[XML.Body]] =
-    tooltips(Rendering.tooltip_elements, range).map(info => info.map(Pretty.fbreaks(_)))
-
-  def tooltip_message(range: Text.Range): Option[Text.Info[XML.Body]] =
-    tooltips(Rendering.tooltip_message_elements, range).map(info => info.map(Pretty.fbreaks(_)))
+  def tooltip(range: Text.Range, control: Boolean): Option[Text.Info[XML.Body]] =
+  {
+    val elements = if (control) Rendering.tooltip_elements else Rendering.tooltip_message_elements
+    tooltips(elements, range).map(info => info.map(Pretty.fbreaks(_)))
+  }
 
   lazy val tooltip_close_icon = JEdit_Lib.load_icon(options.string("tooltip_close_icon"))
   lazy val tooltip_detach_icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon"))
diff -r 633a8d52fef2 -r 5d62f797e40c src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Sat Feb 29 16:30:30 2020 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Sat Feb 29 16:38:59 2020 +0100
@@ -263,10 +263,7 @@
                   JEdit_Lib.pixel_range(text_area, x, y) match {
                     case None =>
                     case Some(range) =>
-                      val result =
-                        if (control) rendering.tooltip(range)
-                        else rendering.tooltip_message(range)
-                      result match {
+                      rendering.tooltip(range, control) match {
                         case None =>
                         case Some(tip) =>
                           val painter = text_area.getPainter