src/Tools/jEdit/src/theories_dockable.scala
changeset 53178 0a3a5f606b2a
parent 53177 dcac8d837b9c
child 53711 8ce7795256e1
     1.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Sat Aug 24 13:32:51 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Sat Aug 24 14:58:36 2013 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  import scala.swing.event.{ButtonClicked, MouseClicked, MouseMoved}
     1.5  
     1.6  import java.lang.System
     1.7 -import java.awt.{BorderLayout, Graphics2D, Insets, Point, Dimension}
     1.8 +import java.awt.{BorderLayout, Graphics2D, Color, Point, Dimension}
     1.9  import javax.swing.{JList, BorderFactory}
    1.10  import javax.swing.border.{BevelBorder, SoftBevelBorder}
    1.11  
    1.12 @@ -137,28 +137,30 @@
    1.13  
    1.14        override def paintComponent(gfx: Graphics2D)
    1.15        {
    1.16 -        val w = size.width
    1.17 -        val h = size.height
    1.18 +        def paint_segment(x: Int, w: Int, color: Color)
    1.19 +        {
    1.20 +          gfx.setColor(color)
    1.21 +          gfx.fillRect(x, 0, w, size.height)
    1.22 +        }
    1.23  
    1.24          nodes_status.get(node_name) match {
    1.25            case Some(st) if st.total > 0 =>
    1.26 -            val colors = List(
    1.27 -              (st.unprocessed, PIDE.options.color_value("unprocessed1_color")),
    1.28 -              (st.running, PIDE.options.color_value("running_color")),
    1.29 -              (st.warned, PIDE.options.color_value("warning_color")),
    1.30 -              (st.failed, PIDE.options.color_value("error_color")))
    1.31 +            val segments =
    1.32 +              List(
    1.33 +                (st.unprocessed, PIDE.options.color_value("unprocessed1_color")),
    1.34 +                (st.running, PIDE.options.color_value("running_color")),
    1.35 +                (st.warned, PIDE.options.color_value("warning_color")),
    1.36 +                (st.failed, PIDE.options.color_value("error_color"))
    1.37 +              ).filter(_._1 > 0)
    1.38  
    1.39 -            var end = size.width
    1.40 -            for { (n, color) <- colors }
    1.41 -            {
    1.42 -              gfx.setColor(color)
    1.43 -              val v = (n * (w - colors.length) / st.total) max (if (n > 0) 4 else 0)
    1.44 -              gfx.fillRect(end - v, 0, v, h)
    1.45 -              end = end - v - 1
    1.46 -            }
    1.47 +            (size.width /: segments)({ case (last, (n, color)) =>
    1.48 +              val w = (n * (size.width - segments.length) / st.total) max 4
    1.49 +              paint_segment(last - w, w, color)
    1.50 +              last - w - 1
    1.51 +            })
    1.52 +
    1.53            case _ =>
    1.54 -            gfx.setColor(PIDE.options.color_value("unprocessed1_color"))
    1.55 -            gfx.fillRect(0, 0, w, h)
    1.56 +            paint_segment(0, size.width, PIDE.options.color_value("unprocessed1_color"))
    1.57          }
    1.58          super.paintComponent(gfx)
    1.59        }