# HG changeset patch
# User wenzelm
# Date 1363601099 -3600
# Node ID e4203ebfe750900c4aefc2757cfb9118c7b9e695
# Parent  a8e3a72b348c42f51e8d3d9808c65cf88e7ace64
recovered special background handling from 8d6e478934dc, particularly relevant for gutter border;

diff -r a8e3a72b348c -r e4203ebfe750 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sun Mar 17 22:02:06 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Mon Mar 18 11:04:59 2013 +0100
@@ -74,6 +74,8 @@
     new Rich_Text_Area(view, text_area, () => current_rendering, close_action,
       caret_visible = false, hovering = true)
 
+  def get_background(): Option[Color] = None
+
   def refresh()
   {
     Swing_Thread.require()
@@ -94,6 +96,7 @@
 
     getGutter.setForeground(jEdit.getColorProperty("view.gutter.fgColor"))
     getGutter.setBackground(jEdit.getColorProperty("view.gutter.bgColor"))
+    get_background().map(bg => { getPainter.setBackground(bg); getGutter.setBackground(bg) })
     getGutter.setHighlightedForeground(jEdit.getColorProperty("view.gutter.highlightColor"))
     getGutter.setFoldColor(jEdit.getColorProperty("view.gutter.foldColor"))
     getGutter.setFont(jEdit.getFontProperty("view.gutter.font"))
diff -r a8e3a72b348c -r e4203ebfe750 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Sun Mar 17 22:02:06 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Mon Mar 18 11:04:59 2013 +0100
@@ -106,7 +106,9 @@
     new JPanel(new BorderLayout) { override def getFocusTraversalKeysEnabled = false }
   window.setContentPane(content_panel)
 
-  val pretty_text_area = new Pretty_Text_Area(view, () => window.dispose(), true)
+  val pretty_text_area = new Pretty_Text_Area(view, () => window.dispose(), true) {
+    override def get_background() = Some(current_rendering.tooltip_color)
+  }
   window.add(pretty_text_area)
 
 
@@ -150,11 +152,8 @@
       Rendering.font_size("jedit_tooltip_font_scale").round)
     pretty_text_area.update(rendering.snapshot, results, body)
 
-    val background = rendering.tooltip_color
-    content_panel.setBackground(background)
-    controls.background = background
-    pretty_text_area.getPainter.setBackground(background)
-    pretty_text_area.getGutter.setBackground(background)
+    content_panel.setBackground(rendering.tooltip_color)
+    controls.background = rendering.tooltip_color
 
 
     /* window geometry */