more uniform tooltip color;

--- 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)