clarified colors, following d6a14ed060fb; default tip
authorwenzelm
Wed, 23 Jul 2025 14:53:21 +0200
changeset 82898 89da4dcd1fa8
parent 82897 9225b889f68a
clarified colors, following d6a14ed060fb;
src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Jul 23 13:21:52 2025 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Jul 23 14:53:21 2025 +0200
@@ -223,7 +223,7 @@
   /* main content */
 
   def tip_border(has_focus: Boolean): Unit = {
-    val color = if (has_focus) GUI.default_background_color() else GUI.default_intermediate_color()
+    val color = if (has_focus) GUI.default_foreground_color() else GUI.default_intermediate_color()
     pretty_tooltip.setBorder(new LineBorder(color))
     pretty_tooltip.repaint()
   }