# HG changeset patch
# User wenzelm
# Date 1731069433 -3600
# Node ID 6b805c746e3bfafeb013e833dedd34206b8cdfd4
# Parent  f92ea68473f2530c118f8fff0c10ddf29698bbb3
tuned signature;

diff -r f92ea68473f2 -r 6b805c746e3b src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Nov 08 13:27:26 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Nov 08 13:37:13 2024 +0100
@@ -28,16 +28,18 @@
   private var stack: List[Pretty_Tooltip] = Nil
 
   private def hierarchy(
-    tip: Pretty_Tooltip
+    pretty_tooltip: Pretty_Tooltip
   ): Option[(List[Pretty_Tooltip], List[Pretty_Tooltip])] = {
     GUI_Thread.require {}
 
-    if (stack.contains(tip)) Some(stack.span(_ != tip))
+    if (stack.contains(pretty_tooltip)) Some(stack.span(_ != pretty_tooltip))
     else None
   }
 
   private def descendant(parent: JComponent): Option[Pretty_Tooltip] =
-    GUI_Thread.require { stack.find(tip => tip.original_parent == parent) }
+    GUI_Thread.require {
+      stack.find(pretty_tooltip => pretty_tooltip.original_parent == parent)
+    }
 
   def apply(
     view: View,
@@ -57,15 +59,16 @@
           case Some(layered) =>
             val (old, rest) =
               GUI.ancestors(parent).collectFirst({ case x: Pretty_Tooltip => x }) match {
-                case Some(tip) => hierarchy(tip).getOrElse((stack, Nil))
+                case Some(pretty_tooltip) => hierarchy(pretty_tooltip).getOrElse((stack, Nil))
                 case None => (stack, Nil)
               }
             old.foreach(_.hide_popup())
 
             val loc = SwingUtilities.convertPoint(parent, location, layered)
-            val tip = new Pretty_Tooltip(view, layered, parent, loc, rendering, results, output)
-            stack = tip :: rest
-            tip.show_popup()
+            val pretty_tooltip =
+              new Pretty_Tooltip(view, layered, parent, loc, rendering, results, output)
+            stack = pretty_tooltip :: rest
+            pretty_tooltip.show_popup()
         }
     }
   }
@@ -117,7 +120,7 @@
     Delay.last(PIDE.session.input_delay, gui = true) { dismiss_unfocused() }
 
   def dismiss_unfocused(): Unit = {
-    stack.span(tip => !tip.pretty_text_area.isFocusOwner) match {
+    stack.span(pretty_tooltip => !pretty_tooltip.pretty_text_area.isFocusOwner) match {
       case (Nil, _) =>
       case (unfocused, rest) =>
         deactivate()
@@ -126,16 +129,16 @@
     }
   }
 
-  def dismiss(tip: Pretty_Tooltip): Unit = {
+  def dismiss(pretty_tooltip: Pretty_Tooltip): Unit = {
     deactivate()
-    hierarchy(tip) match {
+    hierarchy(pretty_tooltip) match {
       case Some((old, _ :: rest)) =>
         rest match {
           case top :: _ => top.request_focus()
           case Nil => JEdit_Lib.request_focus_view()
         }
         old.foreach(_.hide_popup())
-        tip.hide_popup()
+        pretty_tooltip.hide_popup()
         stack = rest
       case _ =>
     }
@@ -166,7 +169,7 @@
   private val results: Command.Results,
   private val output: List[XML.Elem]
 ) extends JPanel(new BorderLayout) {
-  tip =>
+  pretty_tooltip =>
 
   GUI_Thread.require {}
 
@@ -177,7 +180,7 @@
     icon = rendering.tooltip_close_icon
     tooltip = "Close tooltip window"
     listenTo(mouse.clicks)
-    reactions += { case _: MouseClicked => Pretty_Tooltip.dismiss(tip) }
+    reactions += { case _: MouseClicked => Pretty_Tooltip.dismiss(pretty_tooltip) }
   }
 
   private val detach = new Label {
@@ -187,7 +190,7 @@
     reactions += {
       case _: MouseClicked =>
         Info_Dockable(view, rendering.snapshot, results, output)
-        Pretty_Tooltip.dismiss(tip)
+        Pretty_Tooltip.dismiss(pretty_tooltip)
     }
   }
 
@@ -199,7 +202,7 @@
   /* text area */
 
   val pretty_text_area: Pretty_Text_Area =
-    new Pretty_Text_Area(view, () => Pretty_Tooltip.dismiss(tip), true) {
+    new Pretty_Text_Area(view, () => Pretty_Tooltip.dismiss(pretty_tooltip), true) {
       override def get_background(): Option[Color] = Some(rendering.tooltip_color)
     }
 
@@ -220,20 +223,20 @@
   /* main content */
 
   def tip_border(has_focus: Boolean): Unit = {
-    tip.setBorder(new LineBorder(if (has_focus) Color.BLACK else Color.GRAY))
-    tip.repaint()
+    pretty_tooltip.setBorder(new LineBorder(if (has_focus) Color.BLACK else Color.GRAY))
+    pretty_tooltip.repaint()
   }
   tip_border(true)
 
   override def getFocusTraversalKeysEnabled = false
-  tip.setBackground(rendering.tooltip_color)
-  tip.add(controls.peer, BorderLayout.NORTH)
-  tip.add(pretty_text_area)
+  pretty_tooltip.setBackground(rendering.tooltip_color)
+  pretty_tooltip.add(controls.peer, BorderLayout.NORTH)
+  pretty_tooltip.add(pretty_text_area)
 
 
   /* popup */
 
-  private val popup = {
+  private val popup: Popup = {
     val screen = GUI.screen_location(layered, location)
     val size = {
       val bounds = JEdit_Rendering.popup_bounds
@@ -242,7 +245,7 @@
       val h_max = layered.getHeight min (screen.bounds.height * bounds).toInt
 
       val painter = pretty_text_area.getPainter
-      val geometry = JEdit_Lib.window_geometry(tip, painter)
+      val geometry = JEdit_Lib.window_geometry(pretty_tooltip, painter)
       val metric = JEdit_Lib.font_metric(painter)
 
       val margin =
@@ -262,7 +265,7 @@
 
       new Dimension(w min w_max, h min h_max)
     }
-    new Popup(layered, tip, screen.relative(layered, size), size)
+    new Popup(layered, pretty_tooltip, screen.relative(layered, size), size)
   }
 
   private def show_popup(): Unit = {