stronger colors (as background);
authorwenzelm
Sat Sep 10 20:39:13 2011 +0200 (2011-09-10)
changeset 4486779d3d74e7cbb
parent 44866 0eb8284a64bd
child 44869 328825888426
stronger colors (as background);
src/Tools/jEdit/src/session_dockable.scala
     1.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Sat Sep 10 20:22:22 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Sat Sep 10 20:39:13 2011 +0200
     1.3 @@ -90,7 +90,6 @@
     1.4    {
     1.5      override def paintComponent(gfx: Graphics)
     1.6      {
     1.7 -      super.paintComponent(gfx)
     1.8        nodes_status.get(Document.Node.Name(getText, "", "")) match {
     1.9          case Some(st) if st.total > 0 =>
    1.10            val w = getWidth
    1.11 @@ -99,8 +98,8 @@
    1.12            for {
    1.13              (n, color) <- List(
    1.14                (st.unprocessed, Isabelle_Markup.unprocessed1_color),
    1.15 -              (st.running, Isabelle_Markup.running1_color),
    1.16 -              (st.failed, Isabelle_Markup.error1_color)) }
    1.17 +              (st.running, Isabelle_Markup.running_color),
    1.18 +              (st.failed, Isabelle_Markup.error_color)) }
    1.19            {
    1.20              gfx.setColor(color)
    1.21              val v = (n * w / st.total) max (if (n > 0) 2 else 0)
    1.22 @@ -109,6 +108,7 @@
    1.23            }
    1.24          case _ =>
    1.25        }
    1.26 +      super.paintComponent(gfx)
    1.27      }
    1.28    }
    1.29