--- 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"))