# HG changeset patch # User wenzelm # Date 1396543182 -7200 # Node ID e49561ae3b651d5b9978eaf692a9a67c49998784 # Parent c771f0fe28d14d058e8ed827a4cfc088b37ef1e2 tuned rendering for 5 different look-and-feels; diff -r c771f0fe28d1 -r e49561ae3b65 src/Tools/jEdit/src/theories_dockable.scala --- a/src/Tools/jEdit/src/theories_dockable.scala Thu Apr 03 15:40:31 2014 +0200 +++ b/src/Tools/jEdit/src/theories_dockable.scala Thu Apr 03 18:39:42 2014 +0200 @@ -15,8 +15,8 @@ import scala.swing.event.{MouseClicked, MouseMoved} import java.awt.{BorderLayout, Graphics2D, Color, Point, Dimension} -import javax.swing.{JList, BorderFactory} -import javax.swing.border.{BevelBorder, SoftBevelBorder, EtchedBorder} +import javax.swing.{JList, BorderFactory, UIManager} +import javax.swing.border.{BevelBorder, SoftBevelBorder} import org.gjt.sp.jedit.{View, jEdit} @@ -26,6 +26,12 @@ /* status */ private val status = new ListView(Nil: List[Document.Node.Name]) { + background = + { + // enforce default value + val c = UIManager.getDefaults.getColor("Panel.background") + new Color(c.getRed, c.getGreen, c.getBlue, c.getAlpha) + } listenTo(mouse.clicks) listenTo(mouse.moves) reactions += { @@ -109,7 +115,7 @@ private object Node_Renderer_Component extends BorderPanel { - opaque = false + opaque = true border = BorderFactory.createEmptyBorder(2, 2, 2, 2) var node_name = Document.Node.Name.empty @@ -126,8 +132,13 @@ } val label = new Label { + background = view.getTextArea.getPainter.getBackground + foreground = view.getTextArea.getPainter.getForeground + border = + BorderFactory.createCompoundBorder( + BorderFactory.createLineBorder(foreground, 1), + BorderFactory.createEmptyBorder(1, 1, 1, 1)) opaque = false - border = new EtchedBorder(EtchedBorder.RAISED) xAlignment = Alignment.Leading override def paintComponent(gfx: Graphics2D) @@ -138,6 +149,7 @@ gfx.fillRect(x, 0, w, size.height) } + paint_segment(0, size.width, background) nodes_status.get(node_name) match { case Some(st) if st.total > 0 => val segments =