refined status of forked goals;
authorwenzelm
Thu Aug 30 15:26:37 2012 +0200 (2012-08-30 ago)
changeset 4900915381ea111ec
parent 49008 a3cdb49c22cc
child 49010 72808e956879
refined status of forked goals;
src/Pure/Concurrent/future.ML
src/Pure/PIDE/isabelle_markup.ML
src/Pure/PIDE/isabelle_markup.scala
src/Pure/PIDE/protocol.scala
src/Pure/goal.ML
     1.1 --- a/src/Pure/Concurrent/future.ML	Thu Aug 30 15:22:21 2012 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Thu Aug 30 15:26:37 2012 +0200
     1.3 @@ -73,7 +73,6 @@
     1.4    val fulfill_result: 'a future -> 'a Exn.result -> unit
     1.5    val fulfill: 'a future -> 'a -> unit
     1.6    val shutdown: unit -> unit
     1.7 -  val status: (unit -> 'a) -> 'a
     1.8    val group_tasks: group -> task list
     1.9    val queue_status: unit -> {ready: int, pending: int, running: int, passive: int}
    1.10  end;
    1.11 @@ -642,20 +641,6 @@
    1.12    else ();
    1.13  
    1.14  
    1.15 -(* status markup *)
    1.16 -
    1.17 -fun status e =
    1.18 -  let
    1.19 -    val task_props =
    1.20 -      (case worker_task () of
    1.21 -        NONE => I
    1.22 -      | SOME task => Markup.properties [(Isabelle_Markup.taskN, Task_Queue.str_of_task task)]);
    1.23 -    val _ = Output.status (Markup.markup_only (task_props Isabelle_Markup.forked));
    1.24 -    val x = e ();  (*sic -- report "joined" only for success*)
    1.25 -    val _ = Output.status (Markup.markup_only (task_props Isabelle_Markup.joined));
    1.26 -  in x end;
    1.27 -
    1.28 -
    1.29  (* queue status *)
    1.30  
    1.31  fun group_tasks group = Task_Queue.group_tasks (! queue) group;
     2.1 --- a/src/Pure/PIDE/isabelle_markup.ML	Thu Aug 30 15:22:21 2012 +0200
     2.2 +++ b/src/Pure/PIDE/isabelle_markup.ML	Thu Aug 30 15:26:37 2012 +0200
     2.3 @@ -89,6 +89,7 @@
     2.4    val acceptedN: string val accepted: Markup.T
     2.5    val forkedN: string val forked: Markup.T
     2.6    val joinedN: string val joined: Markup.T
     2.7 +  val cancelledN: string val cancelled: Markup.T
     2.8    val failedN: string val failed: Markup.T
     2.9    val finishedN: string val finished: Markup.T
    2.10    val serialN: string
    2.11 @@ -273,7 +274,7 @@
    2.12  val (acceptedN, accepted) = markup_elem "accepted";
    2.13  val (forkedN, forked) = markup_elem "forked";
    2.14  val (joinedN, joined) = markup_elem "joined";
    2.15 -
    2.16 +val (cancelledN, cancelled) = markup_elem "cancelled";
    2.17  val (failedN, failed) = markup_elem "failed";
    2.18  val (finishedN, finished) = markup_elem "finished";
    2.19  
     3.1 --- a/src/Pure/PIDE/isabelle_markup.scala	Thu Aug 30 15:22:21 2012 +0200
     3.2 +++ b/src/Pure/PIDE/isabelle_markup.scala	Thu Aug 30 15:26:37 2012 +0200
     3.3 @@ -195,6 +195,7 @@
     3.4    val ACCEPTED = "accepted"
     3.5    val FORKED = "forked"
     3.6    val JOINED = "joined"
     3.7 +  val CANCELLED = "cancelled"
     3.8    val FAILED = "failed"
     3.9    val FINISHED = "finished"
    3.10  
     4.1 --- a/src/Pure/PIDE/protocol.scala	Thu Aug 30 15:22:21 2012 +0200
     4.2 +++ b/src/Pure/PIDE/protocol.scala	Thu Aug 30 15:26:37 2012 +0200
     4.3 @@ -65,13 +65,14 @@
     4.4  
     4.5    val command_status_markup: Set[String] =
     4.6      Set(Isabelle_Markup.ACCEPTED, Isabelle_Markup.FINISHED, Isabelle_Markup.FAILED,
     4.7 -      Isabelle_Markup.FORKED, Isabelle_Markup.JOINED)
     4.8 +      Isabelle_Markup.FORKED, Isabelle_Markup.JOINED, Isabelle_Markup.CANCELLED)
     4.9  
    4.10    def command_status(status: Status, markup: Markup): Status =
    4.11      markup match {
    4.12        case Markup(Isabelle_Markup.ACCEPTED, _) => status.copy(accepted = true)
    4.13        case Markup(Isabelle_Markup.FINISHED, _) => status.copy(finished = true)
    4.14        case Markup(Isabelle_Markup.FAILED, _) => status.copy(failed = true)
    4.15 +      case Markup(Isabelle_Markup.CANCELLED, _) => status.copy(failed = true)
    4.16        case Markup(Isabelle_Markup.FORKED, _) => status.copy(forks = status.forks + 1)
    4.17        case Markup(Isabelle_Markup.JOINED, _) => status.copy(forks = status.forks - 1)
    4.18        case _ => status
     5.1 --- a/src/Pure/goal.ML	Thu Aug 30 15:22:21 2012 +0200
     5.2 +++ b/src/Pure/goal.ML	Thu Aug 30 15:26:37 2012 +0200
     5.3 @@ -119,6 +119,24 @@
     5.4            ("PROOFS " ^ Time.toString (Time.now ()) ^ ": " ^ string_of_int n));
     5.5      in n end);
     5.6  
     5.7 +fun capture_status e =
     5.8 +  let
     5.9 +    val task_props =
    5.10 +      (case Future.worker_task () of
    5.11 +        NONE => I
    5.12 +      | SOME task => Markup.properties [(Isabelle_Markup.taskN, Task_Queue.str_of_task task)]);
    5.13 +    fun status m = Output.status (Markup.markup_only (task_props m));
    5.14 +
    5.15 +    val _ = status Isabelle_Markup.forked;
    5.16 +    val result = Exn.capture (Future.interruptible_task e) ();
    5.17 +    val _ =
    5.18 +      (case result of
    5.19 +        Exn.Res _ => status Isabelle_Markup.joined
    5.20 +      | Exn.Exn exn =>
    5.21 +          if Exn.is_interrupt exn then status Isabelle_Markup.cancelled
    5.22 +          else status Isabelle_Markup.failed);
    5.23 +  in result end;
    5.24 +
    5.25  fun fork_name name e =
    5.26    uninterruptible (fn _ => fn () =>
    5.27      let
    5.28 @@ -126,9 +144,7 @@
    5.29        val future =
    5.30          (singleton o Future.forks)
    5.31            {name = name, group = NONE, deps = [], pri = ~1, interrupts = false}
    5.32 -          (fn () =>
    5.33 -            Exn.release
    5.34 -              (Exn.capture (Future.status o Future.interruptible_task) e before forked ~1));
    5.35 +          (fn () => Exn.release (capture_status e before forked ~1));
    5.36      in future end) ();
    5.37  
    5.38  fun fork e = fork_name "Goal.fork" e;