clarified border (again, see also 7ce3ebc268a1);
authorwenzelm
Sat Aug 24 12:31:24 2013 +0200 (2013-08-24)
changeset 53176f88635e1c52e
parent 53175 4834c2df9995
child 53177 dcac8d837b9c
clarified border (again, see also 7ce3ebc268a1);
src/Tools/jEdit/src/theories_dockable.scala
     1.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Sat Aug 24 00:06:53 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Sat Aug 24 12:31:24 2013 +0200
     1.3 @@ -114,6 +114,7 @@
     1.4    private object Node_Renderer_Component extends BorderPanel
     1.5    {
     1.6      opaque = false
     1.7 +    border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
     1.8  
     1.9      var node_name = Document.Node.Name.empty
    1.10  
    1.11 @@ -130,15 +131,13 @@
    1.12  
    1.13      val label = new Label {
    1.14        opaque = false
    1.15 +      border = BorderFactory.createEmptyBorder()
    1.16        xAlignment = Alignment.Leading
    1.17  
    1.18        override def paintComponent(gfx: Graphics2D)
    1.19        {
    1.20 -        border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
    1.21 -        val size = peer.getSize()
    1.22 -        val insets = border.getBorderInsets(peer)
    1.23 -        val w = size.width - insets.left - insets.right
    1.24 -        val h = size.height - insets.top - insets.bottom
    1.25 +        val w = size.width
    1.26 +        val h = size.height
    1.27  
    1.28          nodes_status.get(node_name) match {
    1.29            case Some(st) if st.total > 0 =>
    1.30 @@ -148,17 +147,17 @@
    1.31                (st.warned, PIDE.options.color_value("warning_color")),
    1.32                (st.failed, PIDE.options.color_value("error_color")))
    1.33  
    1.34 -            var end = size.width - insets.right
    1.35 +            var end = size.width
    1.36              for { (n, color) <- colors }
    1.37              {
    1.38                gfx.setColor(color)
    1.39                val v = (n * (w - colors.length) / st.total) max (if (n > 0) 4 else 0)
    1.40 -              gfx.fillRect(end - v, insets.top, v, h)
    1.41 +              gfx.fillRect(end - v, 0, v, h)
    1.42                end = end - v - 1
    1.43              }
    1.44            case _ =>
    1.45              gfx.setColor(PIDE.options.color_value("unprocessed1_color"))
    1.46 -            gfx.fillRect(insets.left, insets.top, w, h)
    1.47 +            gfx.fillRect(0, 0, w, h)
    1.48          }
    1.49          super.paintComponent(gfx)
    1.50        }