# HG changeset patch
# User wenzelm
# Date 1375266670 -7200
# Node ID e750169a58848df71960178251d6dccdca9a86f5
# Parent  143f225e50f5861d1e7b8d42f8fd5146b044d47e
paint unassigned/unchanged nodes as unprocessed -- relevant for editor_continuous_checking = false;

diff -r 143f225e50f5 -r e750169a5884 src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Wed Jul 31 12:14:13 2013 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Wed Jul 31 12:31:10 2013 +0200
@@ -82,6 +82,11 @@
     var node_name = Document.Node.Name.empty
     override def paintComponent(gfx: Graphics2D)
     {
+      val size = peer.getSize()
+      val insets = border.getBorderInsets(peer)
+      val w = size.width - insets.left - insets.right
+      val h = size.height - insets.top - insets.bottom
+
       nodes_status.get(node_name) match {
         case Some(st) if st.total > 0 =>
           val colors = List(
@@ -90,12 +95,7 @@
             (st.warned, PIDE.options.color_value("warning_color")),
             (st.failed, PIDE.options.color_value("error_color")))
 
-          val size = peer.getSize()
-          val insets = border.getBorderInsets(peer)
-          val w = size.width - insets.left - insets.right
-          val h = size.height - insets.top - insets.bottom
           var end = size.width - insets.right
-
           for { (n, color) <- colors }
           {
             gfx.setColor(color)
@@ -104,6 +104,8 @@
             end = end - v - 1
           }
         case _ =>
+          gfx.setColor(PIDE.options.color_value("unprocessed1_color"))
+          gfx.fillRect(insets.left, insets.top, w, h)
       }
       super.paintComponent(gfx)
     }