--- a/src/Tools/jEdit/src/session_dockable.scala Fri Sep 14 12:29:02 2012 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala Fri Sep 14 12:46:33 2012 +0200
@@ -89,10 +89,10 @@
var end = size.width - insets.right
for {
(n, color) <- List(
- (st.unprocessed, Isabelle_Rendering.color_value("color_unprocessed1")),
- (st.running, Isabelle_Rendering.color_value("color_running")),
- (st.warned, Isabelle_Rendering.color_value("color_warning")),
- (st.failed, Isabelle_Rendering.color_value("color_error"))) }
+ (st.unprocessed, Isabelle_Rendering.color_value("unprocessed1_color")),
+ (st.running, Isabelle_Rendering.color_value("running_color")),
+ (st.warned, Isabelle_Rendering.color_value("warning_color")),
+ (st.failed, Isabelle_Rendering.color_value("error_color"))) }
{
gfx.setColor(color)
val v = (n * w / st.total) max (if (n > 0) 2 else 0)