# HG changeset patch
# User wenzelm
# Date 1346333197 -7200
# Node ID 15381ea111ecefa2505ead1275c03476eb74a1fb
# Parent  a3cdb49c22ccf8c223f8824acb4e54ee73b6e6da
refined status of forked goals;

diff -r a3cdb49c22cc -r 15381ea111ec src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Thu Aug 30 15:22:21 2012 +0200
+++ b/src/Pure/Concurrent/future.ML	Thu Aug 30 15:26:37 2012 +0200
@@ -73,7 +73,6 @@
   val fulfill_result: 'a future -> 'a Exn.result -> unit
   val fulfill: 'a future -> 'a -> unit
   val shutdown: unit -> unit
-  val status: (unit -> 'a) -> 'a
   val group_tasks: group -> task list
   val queue_status: unit -> {ready: int, pending: int, running: int, passive: int}
 end;
@@ -642,20 +641,6 @@
   else ();
 
 
-(* status markup *)
-
-fun status e =
-  let
-    val task_props =
-      (case worker_task () of
-        NONE => I
-      | SOME task => Markup.properties [(Isabelle_Markup.taskN, Task_Queue.str_of_task task)]);
-    val _ = Output.status (Markup.markup_only (task_props Isabelle_Markup.forked));
-    val x = e ();  (*sic -- report "joined" only for success*)
-    val _ = Output.status (Markup.markup_only (task_props Isabelle_Markup.joined));
-  in x end;
-
-
 (* queue status *)
 
 fun group_tasks group = Task_Queue.group_tasks (! queue) group;
diff -r a3cdb49c22cc -r 15381ea111ec src/Pure/PIDE/isabelle_markup.ML
--- a/src/Pure/PIDE/isabelle_markup.ML	Thu Aug 30 15:22:21 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.ML	Thu Aug 30 15:26:37 2012 +0200
@@ -89,6 +89,7 @@
   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 failedN: string val failed: Markup.T
   val finishedN: string val finished: Markup.T
   val serialN: string
@@ -273,7 +274,7 @@
 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 (failedN, failed) = markup_elem "failed";
 val (finishedN, finished) = markup_elem "finished";
 
diff -r a3cdb49c22cc -r 15381ea111ec src/Pure/PIDE/isabelle_markup.scala
--- a/src/Pure/PIDE/isabelle_markup.scala	Thu Aug 30 15:22:21 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.scala	Thu Aug 30 15:26:37 2012 +0200
@@ -195,6 +195,7 @@
   val ACCEPTED = "accepted"
   val FORKED = "forked"
   val JOINED = "joined"
+  val CANCELLED = "cancelled"
   val FAILED = "failed"
   val FINISHED = "finished"
 
diff -r a3cdb49c22cc -r 15381ea111ec src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Thu Aug 30 15:22:21 2012 +0200
+++ b/src/Pure/PIDE/protocol.scala	Thu Aug 30 15:26:37 2012 +0200
@@ -65,13 +65,14 @@
 
   val command_status_markup: Set[String] =
     Set(Isabelle_Markup.ACCEPTED, Isabelle_Markup.FINISHED, Isabelle_Markup.FAILED,
-      Isabelle_Markup.FORKED, Isabelle_Markup.JOINED)
+      Isabelle_Markup.FORKED, Isabelle_Markup.JOINED, Isabelle_Markup.CANCELLED)
 
   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.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
diff -r a3cdb49c22cc -r 15381ea111ec src/Pure/goal.ML
--- a/src/Pure/goal.ML	Thu Aug 30 15:22:21 2012 +0200
+++ b/src/Pure/goal.ML	Thu Aug 30 15:26:37 2012 +0200
@@ -119,6 +119,24 @@
           ("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 fork_name name e =
   uninterruptible (fn _ => fn () =>
     let
@@ -126,9 +144,7 @@
       val future =
         (singleton o Future.forks)
           {name = name, group = NONE, deps = [], pri = ~1, interrupts = false}
-          (fn () =>
-            Exn.release
-              (Exn.capture (Future.status o Future.interruptible_task) e before forked ~1));
+          (fn () => Exn.release (capture_status e before forked ~1));
     in future end) ();
 
 fun fork e = fork_name "Goal.fork" e;