further refinement of command status, to accomodate forked proofs;

--- a/src/Pure/PIDE/command.ML	Thu Aug 30 22:38:12 2012 +0200
+++ b/src/Pure/PIDE/command.ML	Fri Aug 31 13:23:25 2012 +0200
@@ -105,13 +105,13 @@
       val is_proof = Keyword.is_proof (Toplevel.name_of tr);
 
       val _ = Multithreading.interrupted ();
-      val _ = Toplevel.status tr Isabelle_Markup.forked;
+      val _ = Toplevel.status tr Isabelle_Markup.running;
       val start = Timing.start ();
       val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
       val errs2 = (case result of NONE => [] | SOME st' => check_cmts tr cmts st');
       val errs = errs1 @ errs2;
       val _ = timing tr (Timing.result start);
-      val _ = Toplevel.status tr Isabelle_Markup.joined;
+      val _ = Toplevel.status tr Isabelle_Markup.finished;
       val _ = List.app (Toplevel.error_msg tr) errs;
     in
       (case result of
@@ -122,7 +122,6 @@
           in ((st, malformed'), no_print) end
       | SOME st' =>
           let
-            val _ = Toplevel.status tr Isabelle_Markup.finished;
             val _ = proof_status tr st';
             val do_print =
               not is_init andalso

--- a/src/Pure/PIDE/isabelle_markup.ML	Thu Aug 30 22:38:12 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.ML	Fri Aug 31 13:23:25 2012 +0200
@@ -89,9 +89,9 @@
   val acceptedN: string val accepted: Markup.T
   val forkedN: string val forked: Markup.T
   val joinedN: string val joined: Markup.T
-  val cancelledN: string val cancelled: Markup.T
+  val runningN: string val running: Markup.T
+  val finishedN: string val finished: Markup.T
   val failedN: string val failed: Markup.T
-  val finishedN: string val finished: Markup.T
   val serialN: string
   val legacyN: string val legacy: Markup.T
   val promptN: string val prompt: Markup.T
@@ -274,9 +274,9 @@
 val (acceptedN, accepted) = markup_elem "accepted";
 val (forkedN, forked) = markup_elem "forked";
 val (joinedN, joined) = markup_elem "joined";
-val (cancelledN, cancelled) = markup_elem "cancelled";
+val (runningN, running) = markup_elem "running";
+val (finishedN, finished) = markup_elem "finished";
 val (failedN, failed) = markup_elem "failed";
-val (finishedN, finished) = markup_elem "finished";
 
 
 (* messages *)

--- a/src/Pure/PIDE/isabelle_markup.scala	Thu Aug 30 22:38:12 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.scala	Fri Aug 31 13:23:25 2012 +0200
@@ -195,9 +195,9 @@
   val ACCEPTED = "accepted"
   val FORKED = "forked"
   val JOINED = "joined"
-  val CANCELLED = "cancelled"
+  val RUNNING = "running"
+  val FINISHED = "finished"
   val FAILED = "failed"
-  val FINISHED = "finished"
 
 
   /* interactive documents */

--- a/src/Pure/PIDE/protocol.scala	Thu Aug 30 22:38:12 2012 +0200
+++ b/src/Pure/PIDE/protocol.scala	Fri Aug 31 13:23:25 2012 +0200
@@ -49,32 +49,34 @@
   }
 
   sealed case class Status(
+    private val touched: Boolean = false,
     private val accepted: Boolean = false,
-    private val finished: Boolean = false,
     private val failed: Boolean = false,
-    forks: Int = 0)
+    forks: Int = 0,
+    runs: Int = 0)
   {
-    def is_unprocessed: Boolean = accepted && !finished && !failed && forks == 0
-    def is_running: Boolean = forks != 0
-    def is_finished: Boolean = finished && forks == 0
-    def is_failed: Boolean = failed && forks == 0
     def + (that: Status): Status =
-      Status(accepted || that.accepted, finished || that.finished,
-        failed || that.failed, forks + that.forks)
+      Status(touched || that.touched, accepted || that.accepted, failed || that.failed,
+        forks + that.forks, runs + that.runs)
+
+    def is_unprocessed: Boolean = accepted && !failed && (!touched || (forks != 0 && runs == 0))
+    def is_running: Boolean = runs != 0
+    def is_finished: Boolean = !failed && forks == 0 && runs == 0
+    def is_failed: Boolean = failed
   }
 
   val command_status_markup: Set[String] =
-    Set(Isabelle_Markup.ACCEPTED, Isabelle_Markup.FINISHED, Isabelle_Markup.FAILED,
-      Isabelle_Markup.FORKED, Isabelle_Markup.JOINED, Isabelle_Markup.CANCELLED)
+    Set(Isabelle_Markup.ACCEPTED, Isabelle_Markup.FORKED, Isabelle_Markup.JOINED,
+      Isabelle_Markup.RUNNING, Isabelle_Markup.FINISHED, Isabelle_Markup.FAILED)
 
   def command_status(status: Status, markup: Markup): Status =
     markup match {
       case Markup(Isabelle_Markup.ACCEPTED, _) => status.copy(accepted = true)
-      case Markup(Isabelle_Markup.FINISHED, _) => status.copy(finished = true)
+      case Markup(Isabelle_Markup.FORKED, _) => status.copy(touched = true, forks = status.forks + 1)
+      case Markup(Isabelle_Markup.JOINED, _) => status.copy(forks = status.forks - 1)
+      case Markup(Isabelle_Markup.RUNNING, _) => status.copy(touched = true, runs = status.runs + 1)
+      case Markup(Isabelle_Markup.FINISHED, _) => status.copy(runs = status.runs - 1)
       case Markup(Isabelle_Markup.FAILED, _) => status.copy(failed = true)
-      case Markup(Isabelle_Markup.CANCELLED, _) => status.copy(failed = true)
-      case Markup(Isabelle_Markup.FORKED, _) => status.copy(forks = status.forks + 1)
-      case Markup(Isabelle_Markup.JOINED, _) => status.copy(forks = status.forks - 1)
       case _ => status
     }
 

--- a/src/Pure/goal.ML	Thu Aug 30 22:38:12 2012 +0200
+++ b/src/Pure/goal.ML	Fri Aug 31 13:23:25 2012 +0200
@@ -120,23 +120,9 @@
           ("PROOFS " ^ Time.toString (Time.now ()) ^ ": " ^ string_of_int n));
     in n end);
 
-fun capture_status e =
-  let
-    val task_props =
-      (case Future.worker_task () of
-        NONE => I
-      | SOME task => Markup.properties [(Isabelle_Markup.taskN, Task_Queue.str_of_task task)]);
-    fun status m = Output.status (Markup.markup_only (task_props m));
-
-    val _ = status Isabelle_Markup.forked;
-    val result = Exn.capture (Future.interruptible_task e) ();
-    val _ =
-      (case result of
-        Exn.Res _ => status Isabelle_Markup.joined
-      | Exn.Exn exn =>
-          if Exn.is_interrupt exn then status Isabelle_Markup.cancelled
-          else status Isabelle_Markup.failed);
-  in result end;
+fun status task markups =
+  let val props = Markup.properties [(Isabelle_Markup.taskN, Task_Queue.str_of_task task)]
+  in Output.status (implode (map (Markup.markup_only o props) markups)) end;
 
 fun fork_name name e =
   uninterruptible (fn _ => fn () =>
@@ -145,7 +131,17 @@
       val future =
         (singleton o Future.forks)
           {name = name, group = NONE, deps = [], pri = ~1, interrupts = false}
-          (fn () => Exn.release (capture_status e before forked ~1));
+          (fn () =>
+            let
+              val task = the (Future.worker_task ());
+              val _ = status task [Isabelle_Markup.running];
+              val result = Exn.capture (Future.interruptible_task e) ();
+              val _ =
+                status task
+                  ([Isabelle_Markup.finished, Isabelle_Markup.joined] @
+                    (if is_some (Exn.get_res result) then [] else [Isabelle_Markup.failed]));
+            in Exn.release result end);
+      val _ = status (Future.task_of future) [Isabelle_Markup.forked];
     in future end) ();
 
 fun fork e = fork_name "Goal.fork" e;

--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Thu Aug 30 22:38:12 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Fri Aug 31 13:23:25 2012 +0200
@@ -293,8 +293,8 @@
         color <-
           (result match {
             case (Some(status), _) =>
-              if (status.is_running) Some(running1_color)
-              else if (status.is_unprocessed) Some(unprocessed1_color)
+              if (status.is_unprocessed) Some(unprocessed1_color)
+              else if (status.is_running) Some(running1_color)
               else None
             case (_, opt_color) => opt_color
           })