explicit running_color;
stronger colors for overview, more transparent colors for status within text;
--- 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
--- 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 =>