# HG changeset patch
# User wenzelm
# Date 1315679953 -7200
# Node ID 79d3d74e7cbb4bff84bc1c495bef1d2a28626693
# Parent  0eb8284a64bd8394bdd88d2868ca8a532ecf4860
stronger colors (as background);

diff -r 0eb8284a64bd -r 79d3d74e7cbb src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Sat Sep 10 20:22:22 2011 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Sat Sep 10 20:39:13 2011 +0200
@@ -90,7 +90,6 @@
   {
     override def paintComponent(gfx: Graphics)
     {
-      super.paintComponent(gfx)
       nodes_status.get(Document.Node.Name(getText, "", "")) match {
         case Some(st) if st.total > 0 =>
           val w = getWidth
@@ -99,8 +98,8 @@
           for {
             (n, color) <- List(
               (st.unprocessed, Isabelle_Markup.unprocessed1_color),
-              (st.running, Isabelle_Markup.running1_color),
-              (st.failed, Isabelle_Markup.error1_color)) }
+              (st.running, Isabelle_Markup.running_color),
+              (st.failed, Isabelle_Markup.error_color)) }
           {
             gfx.setColor(color)
             val v = (n * w / st.total) max (if (n > 0) 2 else 0)
@@ -109,6 +108,7 @@
           }
         case _ =>
       }
+      super.paintComponent(gfx)
     }
   }