paint unassigned/unchanged nodes as unprocessed -- relevant for editor_continuous_checking = false;
authorwenzelm
Wed Jul 31 12:31:10 2013 +0200 (2013-07-31)
changeset 52809e750169a5884
parent 52808 143f225e50f5
child 52810 cd28423ba19f
paint unassigned/unchanged nodes as unprocessed -- relevant for editor_continuous_checking = false;
src/Tools/jEdit/src/theories_dockable.scala
     1.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Wed Jul 31 12:14:13 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Wed Jul 31 12:31:10 2013 +0200
     1.3 @@ -82,6 +82,11 @@
     1.4      var node_name = Document.Node.Name.empty
     1.5      override def paintComponent(gfx: Graphics2D)
     1.6      {
     1.7 +      val size = peer.getSize()
     1.8 +      val insets = border.getBorderInsets(peer)
     1.9 +      val w = size.width - insets.left - insets.right
    1.10 +      val h = size.height - insets.top - insets.bottom
    1.11 +
    1.12        nodes_status.get(node_name) match {
    1.13          case Some(st) if st.total > 0 =>
    1.14            val colors = List(
    1.15 @@ -90,12 +95,7 @@
    1.16              (st.warned, PIDE.options.color_value("warning_color")),
    1.17              (st.failed, PIDE.options.color_value("error_color")))
    1.18  
    1.19 -          val size = peer.getSize()
    1.20 -          val insets = border.getBorderInsets(peer)
    1.21 -          val w = size.width - insets.left - insets.right
    1.22 -          val h = size.height - insets.top - insets.bottom
    1.23            var end = size.width - insets.right
    1.24 -
    1.25            for { (n, color) <- colors }
    1.26            {
    1.27              gfx.setColor(color)
    1.28 @@ -104,6 +104,8 @@
    1.29              end = end - v - 1
    1.30            }
    1.31          case _ =>
    1.32 +          gfx.setColor(PIDE.options.color_value("unprocessed1_color"))
    1.33 +          gfx.fillRect(insets.left, insets.top, w, h)
    1.34        }
    1.35        super.paintComponent(gfx)
    1.36      }