# HG changeset patch
# User wenzelm
# Date 1667991932 -3600
# Node ID 304ae1a6e160ce3c03452466e82b88ba95012b4b
# Parent  3d281371b2137ddb947a1cef789693b041201f34
tuned signature, following hints by IntelliJ IDEA;

diff -r 3d281371b213 -r 304ae1a6e160 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Tue Nov 08 08:41:48 2022 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Nov 09 12:05:32 2022 +0100
@@ -60,12 +60,12 @@
                 case Some(tip) => hierarchy(tip).getOrElse((stack, Nil))
                 case None => (stack, Nil)
               }
-            old.foreach(_.hide_popup)
+            old.foreach(_.hide_popup())
 
             val loc = SwingUtilities.convertPoint(parent, location, layered)
             val tip = new Pretty_Tooltip(view, layered, parent, loc, rendering, results, info)
             stack = tip :: rest
-            tip.show_popup
+            tip.show_popup()
         }
     }
   }
@@ -123,7 +123,7 @@
       case (Nil, _) =>
       case (unfocused, rest) =>
         deactivate()
-        unfocused.foreach(_.hide_popup)
+        unfocused.foreach(_.hide_popup())
         stack = rest
     }
   }
@@ -133,11 +133,11 @@
     hierarchy(tip) match {
       case Some((old, _ :: rest)) =>
         rest match {
-          case top :: _ => top.request_focus
+          case top :: _ => top.request_focus()
           case Nil => JEdit_Lib.request_focus_view()
         }
-        old.foreach(_.hide_popup)
-        tip.hide_popup
+        old.foreach(_.hide_popup())
+        tip.hide_popup()
         stack = rest
       case _ =>
     }
@@ -151,7 +151,7 @@
     if (stack.isEmpty) false
     else {
       JEdit_Lib.request_focus_view()
-      stack.foreach(_.hide_popup)
+      stack.foreach(_.hide_popup())
       stack = Nil
       true
     }
@@ -202,7 +202,7 @@
 
   val pretty_text_area: Pretty_Text_Area =
     new Pretty_Text_Area(view, () => Pretty_Tooltip.dismiss(tip), true) {
-      override def get_background() = Some(rendering.tooltip_color)
+      override def get_background(): Option[Color] = Some(rendering.tooltip_color)
     }
 
   pretty_text_area.addFocusListener(new FocusAdapter {
@@ -269,14 +269,14 @@
     new Popup(layered, tip, screen.relative(layered, size), size)
   }
 
-  private def show_popup: Unit = {
+  private def show_popup(): Unit = {
     popup.show
     pretty_text_area.requestFocus()
     pretty_text_area.update(rendering.snapshot, results, info.info)
   }
 
-  private def hide_popup: Unit = popup.hide
+  private def hide_popup(): Unit = popup.hide
 
-  private def request_focus: Unit = pretty_text_area.requestFocus()
+  private def request_focus(): Unit = pretty_text_area.requestFocus()
 }