# HG changeset patch
# User wenzelm
# Date 1314815544 -7200
# Node ID 857c52a1c3f7bb35e83935f766cdb9ca063ca528
# Parent  49657380fba6af6109b6a1dbbc841f75a572bff0
explicit running_color;
stronger colors for overview, more transparent colors for status within text;

diff -r 49657380fba6 -r 857c52a1c3f7 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Wed Aug 31 19:52:13 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Wed Aug 31 20:32:24 2011 +0200
@@ -345,11 +345,13 @@
     val is_proof = Keyword.is_proof (Toplevel.name_of tr);
     val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof);
 
+    val _ = Toplevel.status tr Markup.forked;
     val start = Timing.start ();
     val (errs, result) =
       if Toplevel.is_toplevel st andalso not is_init then ([], SOME st)
       else run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
     val _ = timing tr (Timing.result start);
+    val _ = Toplevel.status tr Markup.joined;
     val _ = List.app (Toplevel.error_msg tr) errs;
   in
     (case result of
diff -r 49657380fba6 -r 857c52a1c3f7 src/Tools/jEdit/src/isabelle_markup.scala
--- a/src/Tools/jEdit/src/isabelle_markup.scala	Wed Aug 31 19:52:13 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_markup.scala	Wed Aug 31 20:32:24 2011 +0200
@@ -24,7 +24,11 @@
   def get_color(s: String): Color = ColorFactory.getInstance.getColor(s)
 
   val outdated_color = new Color(238, 227, 227)
-  val unfinished_color = new Color(255, 228, 225)
+  val outdated1_color = new Color(238, 227, 227, 50)
+  val running_color = new Color(97, 0, 97)
+  val running1_color = new Color(97, 0, 97, 100)
+  val unfinished_color = new Color(255, 160, 160)
+  val unfinished1_color = new Color(255, 160, 160, 50)
 
   val light_color = new Color(240, 240, 240)
   val regular_color = new Color(192, 192, 192)
@@ -53,11 +57,11 @@
   def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
   {
     val state = snapshot.command_state(command)
-    if (snapshot.is_outdated) Some(outdated_color)
+    if (snapshot.is_outdated) Some(outdated1_color)
     else
       Isar_Document.command_status(state.status) match {
-        case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
-        case Isar_Document.Unprocessed => Some(unfinished_color)
+        case Isar_Document.Forked(i) if i > 0 => Some(running1_color)
+        case Isar_Document.Unprocessed => Some(unfinished1_color)
         case _ => None
       }
   }
@@ -68,7 +72,7 @@
     if (snapshot.is_outdated) None
     else
       Isar_Document.command_status(state.status) match {
-        case Isar_Document.Forked(i) => if (i > 0) Some(unfinished_color) else None
+        case Isar_Document.Forked(i) => if (i > 0) Some(running_color) else None
         case Isar_Document.Unprocessed => Some(unfinished_color)
         case Isar_Document.Failed => Some(error_color)
         case Isar_Document.Finished =>