tuned rendering for 5 different look-and-feels;
authorwenzelm
Thu Apr 03 18:39:42 2014 +0200 (2014-04-03)
changeset 56389e49561ae3b65
parent 56388 c771f0fe28d1
child 56390 8185044353fd
tuned rendering for 5 different look-and-feels;
src/Tools/jEdit/src/theories_dockable.scala
     1.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Thu Apr 03 15:40:31 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Thu Apr 03 18:39:42 2014 +0200
     1.3 @@ -15,8 +15,8 @@
     1.4  import scala.swing.event.{MouseClicked, MouseMoved}
     1.5  
     1.6  import java.awt.{BorderLayout, Graphics2D, Color, Point, Dimension}
     1.7 -import javax.swing.{JList, BorderFactory}
     1.8 -import javax.swing.border.{BevelBorder, SoftBevelBorder, EtchedBorder}
     1.9 +import javax.swing.{JList, BorderFactory, UIManager}
    1.10 +import javax.swing.border.{BevelBorder, SoftBevelBorder}
    1.11  
    1.12  import org.gjt.sp.jedit.{View, jEdit}
    1.13  
    1.14 @@ -26,6 +26,12 @@
    1.15    /* status */
    1.16  
    1.17    private val status = new ListView(Nil: List[Document.Node.Name]) {
    1.18 +    background =
    1.19 +    {
    1.20 +      // enforce default value
    1.21 +      val c = UIManager.getDefaults.getColor("Panel.background")
    1.22 +      new Color(c.getRed, c.getGreen, c.getBlue, c.getAlpha)
    1.23 +    }
    1.24      listenTo(mouse.clicks)
    1.25      listenTo(mouse.moves)
    1.26      reactions += {
    1.27 @@ -109,7 +115,7 @@
    1.28  
    1.29    private object Node_Renderer_Component extends BorderPanel
    1.30    {
    1.31 -    opaque = false
    1.32 +    opaque = true
    1.33      border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
    1.34  
    1.35      var node_name = Document.Node.Name.empty
    1.36 @@ -126,8 +132,13 @@
    1.37      }
    1.38  
    1.39      val label = new Label {
    1.40 +      background = view.getTextArea.getPainter.getBackground
    1.41 +      foreground = view.getTextArea.getPainter.getForeground
    1.42 +      border =
    1.43 +        BorderFactory.createCompoundBorder(
    1.44 +          BorderFactory.createLineBorder(foreground, 1),
    1.45 +          BorderFactory.createEmptyBorder(1, 1, 1, 1))
    1.46        opaque = false
    1.47 -      border = new EtchedBorder(EtchedBorder.RAISED)
    1.48        xAlignment = Alignment.Leading
    1.49  
    1.50        override def paintComponent(gfx: Graphics2D)
    1.51 @@ -138,6 +149,7 @@
    1.52            gfx.fillRect(x, 0, w, size.height)
    1.53          }
    1.54  
    1.55 +        paint_segment(0, size.width, background)
    1.56          nodes_status.get(node_name) match {
    1.57            case Some(st) if st.total > 0 =>
    1.58              val segments =