--- 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;
--- 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";
--- 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"
--- 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
--- 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;