# HG changeset patch
# User wenzelm
# Date 1230489471 -3600
# Node ID 39cb4ed5183bb64b27de4ceb9569f926c39029bc
# Parent  dc8b486fde9ff9659d10aaf84bf5fd8ad78a00ba
command state color: use PG 4.0 values;

diff -r dc8b486fde9f -r 39cb4ed5183b src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Sun Dec 28 19:26:18 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Sun Dec 28 19:37:51 2008 +0100
@@ -28,12 +28,11 @@
 object TheoryView {
 
   def choose_color(state: Command): Color = {
-    if (state == null)
-      Color.red
+    if (state == null) Color.red
     else
       state.phase match {
-        case Phase.UNPROCESSED => new Color(255, 255, 192)
-        case Phase.FINISHED => new Color(192, 255, 192)
+        case Phase.UNPROCESSED => new Color(255, 228, 225)
+        case Phase.FINISHED => new Color(234, 248, 255)
         case Phase.FAILED => new Color(255, 192, 192)
         case _ => Color.red
       }