# HG changeset patch
# User wenzelm
# Date 1747420312 -7200
# Node ID 49e4ce0c6aa13792506244c1a7d5da7fd148e955
# Parent  dc7efd56454427b3356dd42203afd9015105be08
clarified tooltip colors;

diff -r dc7efd564544 -r 49e4ce0c6aa1 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Fri May 16 12:41:42 2025 +0200
+++ b/src/Tools/jEdit/etc/options	Fri May 16 20:31:52 2025 +0200
@@ -93,7 +93,6 @@
 option running_color : string = "610061FF" for color_dialog
 option running1_color : string = "61006164" for color_dialog
 option bullet_color : string = "000000FF" for color_dialog
-option tooltip_color : string = "FFFFE9FF" for color_dialog
 option writeln_color : string = "C0C0C0FF" for color_dialog
 option information_color : string = "C1DFEEFF" for color_dialog
 option warning_color : string = "FF8C00FF" for color_dialog
@@ -162,7 +161,6 @@
 option running_color_dark : string = "7FBFFF00" for color_dialog
 option running1_color_dark : string = "590259FF" for color_dialog
 option bullet_color_dark : string = "EAEAEAFF" for color_dialog
-option tooltip_color_dark : string = "2B2B2BFF" for color_dialog
 option writeln_color_dark : string = "9C9C9CFF" for color_dialog
 option information_color_dark : string = "77B800FF" for color_dialog
 option warning_color_dark : string = "FF8C00FF" for color_dialog
diff -r dc7efd564544 -r 49e4ce0c6aa1 src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Fri May 16 12:41:42 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Fri May 16 20:31:52 2025 +0200
@@ -11,7 +11,7 @@
 import isabelle._
 
 import java.awt.Color
-import javax.swing.Icon
+import javax.swing.{Icon, UIManager}
 
 import org.gjt.sp.jedit.syntax.{Token => JEditToken}
 import org.gjt.sp.jedit.jEdit
@@ -177,7 +177,6 @@
 
   val outdated_color = color("outdated_color")
   val bullet_color = color("bullet_color")
-  val tooltip_color = color("tooltip_color")
   val spell_checker_color = color("spell_checker_color")
   val entity_ref_color = color("entity_ref_color")
   val breakpoint_disabled_color = color("breakpoint_disabled_color")
@@ -190,6 +189,12 @@
   val completion_color = color("completion_color")
   val search_color = color("search_color")
 
+  lazy val tooltip_foreground_color: Color =
+    Option(UIManager.getColor("ToolTip.foreground")).getOrElse(GUI.default_foreground_color())
+
+  lazy val tooltip_background_color: Color =
+    Option(UIManager.getColor("ToolTip.background")).getOrElse(GUI.default_background_color())
+
 
   /* indentation */
 
diff -r dc7efd564544 -r 49e4ce0c6aa1 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Fri May 16 12:41:42 2025 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Fri May 16 20:31:52 2025 +0200
@@ -194,7 +194,8 @@
   }
 
   private val controls = new FlowPanel(FlowPanel.Alignment.Left)(close, detach) {
-    background = rendering.tooltip_color
+    foreground = rendering.tooltip_foreground_color
+    background = rendering.tooltip_background_color
   }
 
 
@@ -202,7 +203,7 @@
 
   val pretty_text_area: Pretty_Text_Area =
     new Pretty_Text_Area(view, () => Pretty_Tooltip.dismiss(pretty_tooltip), true) {
-      override def get_background(): Option[Color] = Some(rendering.tooltip_color)
+      override def get_background(): Option[Color] = Some(rendering.tooltip_background_color)
     }
 
   pretty_text_area.addFocusListener(new FocusAdapter {
@@ -222,14 +223,14 @@
   /* main content */
 
   def tip_border(has_focus: Boolean): Unit = {
-    val color = if (has_focus) GUI.default_foreground_color() else GUI.default_intermediate_color()
+    val color = if (has_focus) GUI.default_background_color() else GUI.default_intermediate_color()
     pretty_tooltip.setBorder(new LineBorder(color))
     pretty_tooltip.repaint()
   }
   tip_border(true)
 
   override def getFocusTraversalKeysEnabled = false
-  pretty_tooltip.setBackground(rendering.tooltip_color)
+  pretty_tooltip.setBackground(rendering.tooltip_background_color)
   pretty_tooltip.add(controls.peer, BorderLayout.NORTH)
   pretty_tooltip.add(pretty_text_area)