# HG changeset patch
# User wenzelm
# Date 1350075200 -7200
# Node ID a974f66062c87aeb6d9028a78800b45b9fea51f3
# Parent  18cb42182d3e5fcc4622a742d5d80d0e3c524e0e
more uniform tooltip color;

diff -r 18cb42182d3e -r a974f66062c8 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Oct 12 22:10:45 2012 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Oct 12 22:53:20 2012 +0200
@@ -55,6 +55,7 @@
   }
 
   window.setContentPane(new JPanel(new BorderLayout) {
+    setBackground(rendering.tooltip_color)
     registerKeyboardAction(action_listener, "close_all",
       KeyStroke.getKeyStroke(KeyEvent.VK_ESCAPE, 0), JComponent.WHEN_FOCUSED)
 
@@ -95,7 +96,9 @@
     }
   }
 
-  private val controls = new FlowPanel(FlowPanel.Alignment.Left)(close, detach)
+  private val controls = new FlowPanel(FlowPanel.Alignment.Left)(close, detach) {
+    background = rendering.tooltip_color
+  }
   window.add(controls.peer, BorderLayout.NORTH)