merged
authorhuffman
Fri Aug 19 16:55:43 2011 -0700 (2011-08-19)
changeset 44315349842366154
parent 44314 dbad46932536
parent 44309 d4decbd67703
child 44316 84b6f7a6cea4
merged
     1.1 --- a/src/Pure/Concurrent/future.ML	Fri Aug 19 15:54:43 2011 -0700
     1.2 +++ b/src/Pure/Concurrent/future.ML	Fri Aug 19 16:55:43 2011 -0700
     1.3 @@ -31,6 +31,9 @@
     1.4      that lack regular result information, will pick up parallel
     1.5      exceptions from the cumulative group context (as Par_Exn).
     1.6  
     1.7 +  * Future task groups may be canceled: present and future group
     1.8 +    members will be interrupted eventually.
     1.9 +
    1.10    * Promised "passive" futures are fulfilled by external means.  There
    1.11      is no associated evaluation task, but other futures can depend on
    1.12      them via regular join operations.
    1.13 @@ -38,31 +41,35 @@
    1.14  
    1.15  signature FUTURE =
    1.16  sig
    1.17 -  val worker_task: unit -> Task_Queue.task option
    1.18 -  val worker_group: unit -> Task_Queue.group option
    1.19 -  val worker_subgroup: unit -> Task_Queue.group
    1.20 +  type task = Task_Queue.task
    1.21 +  type group = Task_Queue.group
    1.22 +  val new_group: group option -> group
    1.23 +  val worker_task: unit -> task option
    1.24 +  val worker_group: unit -> group option
    1.25 +  val worker_subgroup: unit -> group
    1.26    type 'a future
    1.27 -  val task_of: 'a future -> Task_Queue.task
    1.28 +  val task_of: 'a future -> task
    1.29    val peek: 'a future -> 'a Exn.result option
    1.30    val is_finished: 'a future -> bool
    1.31    val get_finished: 'a future -> 'a
    1.32    val interruptible_task: ('a -> 'b) -> 'a -> 'b
    1.33 -  val cancel_group: Task_Queue.group -> unit
    1.34 -  val cancel: 'a future -> unit
    1.35 +  val cancel_group: group -> task list
    1.36 +  val cancel: 'a future -> task list
    1.37    type fork_params =
    1.38 -   {name: string, group: Task_Queue.group option, deps: Task_Queue.task list,
    1.39 -    pri: int, interrupts: bool}
    1.40 +    {name: string, group: group option, deps: task list, pri: int, interrupts: bool}
    1.41    val forks: fork_params -> (unit -> 'a) list -> 'a future list
    1.42    val fork_pri: int -> (unit -> 'a) -> 'a future
    1.43    val fork: (unit -> 'a) -> 'a future
    1.44    val join_results: 'a future list -> 'a Exn.result list
    1.45    val join_result: 'a future -> 'a Exn.result
    1.46    val join: 'a future -> 'a
    1.47 +  val join_tasks: task list -> unit
    1.48 +  val value_result: 'a Exn.result -> 'a future
    1.49    val value: 'a -> 'a future
    1.50    val map: ('a -> 'b) -> 'a future -> 'b future
    1.51    val cond_forks: fork_params -> (unit -> 'a) list -> 'a future list
    1.52 -  val promise_group: Task_Queue.group -> 'a future
    1.53 -  val promise: unit -> 'a future
    1.54 +  val promise_group: group -> (unit -> unit) -> 'a future
    1.55 +  val promise: (unit -> unit) -> 'a future
    1.56    val fulfill_result: 'a future -> 'a Exn.result -> unit
    1.57    val fulfill: 'a future -> 'a -> unit
    1.58    val shutdown: unit -> unit
    1.59 @@ -74,17 +81,22 @@
    1.60  
    1.61  (** future values **)
    1.62  
    1.63 +type task = Task_Queue.task;
    1.64 +type group = Task_Queue.group;
    1.65 +val new_group = Task_Queue.new_group;
    1.66 +
    1.67 +
    1.68  (* identifiers *)
    1.69  
    1.70  local
    1.71 -  val tag = Universal.tag () : Task_Queue.task option Universal.tag;
    1.72 +  val tag = Universal.tag () : task option Universal.tag;
    1.73  in
    1.74    fun worker_task () = the_default NONE (Thread.getLocal tag);
    1.75    fun setmp_worker_task task f x = setmp_thread_data tag (worker_task ()) (SOME task) f x;
    1.76  end;
    1.77  
    1.78  val worker_group = Option.map Task_Queue.group_of_task o worker_task;
    1.79 -fun worker_subgroup () = Task_Queue.new_group (worker_group ());
    1.80 +fun worker_subgroup () = new_group (worker_group ());
    1.81  
    1.82  fun worker_joining e =
    1.83    (case worker_task () of
    1.84 @@ -103,7 +115,7 @@
    1.85  
    1.86  datatype 'a future = Future of
    1.87   {promised: bool,
    1.88 -  task: Task_Queue.task,
    1.89 +  task: task,
    1.90    result: 'a result};
    1.91  
    1.92  fun task_of (Future {task, ...}) = task;
    1.93 @@ -157,7 +169,7 @@
    1.94  val queue = Unsynchronized.ref Task_Queue.empty;
    1.95  val next = Unsynchronized.ref 0;
    1.96  val scheduler = Unsynchronized.ref (NONE: Thread.thread option);
    1.97 -val canceled = Unsynchronized.ref ([]: Task_Queue.group list);
    1.98 +val canceled = Unsynchronized.ref ([]: group list);
    1.99  val do_shutdown = Unsynchronized.ref false;
   1.100  val max_workers = Unsynchronized.ref 0;
   1.101  val max_active = Unsynchronized.ref 0;
   1.102 @@ -172,15 +184,6 @@
   1.103  
   1.104  (* cancellation primitives *)
   1.105  
   1.106 -fun interruptible_task f x =
   1.107 -  if Multithreading.available then
   1.108 -    Multithreading.with_attributes
   1.109 -      (if is_some (worker_task ())
   1.110 -       then Multithreading.private_interrupts
   1.111 -       else Multithreading.public_interrupts)
   1.112 -      (fn _ => f x)
   1.113 -  else interruptible f x;
   1.114 -
   1.115  fun cancel_now group = (*requires SYNCHRONIZED*)
   1.116    Task_Queue.cancel (! queue) group;
   1.117  
   1.118 @@ -189,6 +192,17 @@
   1.119    broadcast scheduler_event);
   1.120  
   1.121  
   1.122 +fun interruptible_task f x =
   1.123 +  (if Multithreading.available then
   1.124 +    Multithreading.with_attributes
   1.125 +      (if is_some (worker_task ())
   1.126 +       then Multithreading.private_interrupts
   1.127 +       else Multithreading.public_interrupts)
   1.128 +      (fn _ => f x)
   1.129 +   else interruptible f x)
   1.130 +  before Multithreading.interrupted ();
   1.131 +
   1.132 +
   1.133  (* worker threads *)
   1.134  
   1.135  fun worker_exec (task, jobs) =
   1.136 @@ -208,10 +222,10 @@
   1.137      val _ = SYNCHRONIZED "finish" (fn () =>
   1.138        let
   1.139          val maximal = Unsynchronized.change_result queue (Task_Queue.finish task);
   1.140 -        val _ = Exn.capture Multithreading.interrupted ();
   1.141 +        val test = Exn.capture Multithreading.interrupted ();
   1.142          val _ =
   1.143 -          if ok then ()
   1.144 -          else if cancel_now group then ()
   1.145 +          if ok andalso not (Exn.is_interrupt_exn test) then ()
   1.146 +          else if null (cancel_now group) then ()
   1.147            else cancel_later group;
   1.148          val _ = broadcast work_finished;
   1.149          val _ = if maximal then () else signal work_available;
   1.150 @@ -244,7 +258,7 @@
   1.151  fun worker_loop name =
   1.152    (case SYNCHRONIZED name (fn () => worker_next ()) of
   1.153      NONE => ()
   1.154 -  | SOME work => (Exn.capture Multithreading.interrupted (); worker_exec work; worker_loop name));
   1.155 +  | SOME work => (worker_exec work; worker_loop name));
   1.156  
   1.157  fun worker_start name = (*requires SYNCHRONIZED*)
   1.158    Unsynchronized.change workers (cons (Simple_Thread.fork false (fn () => worker_loop name),
   1.159 @@ -345,7 +359,7 @@
   1.160        else
   1.161         (Multithreading.tracing 1 (fn () =>
   1.162            string_of_int (length (! canceled)) ^ " canceled groups");
   1.163 -        Unsynchronized.change canceled (filter_out cancel_now);
   1.164 +        Unsynchronized.change canceled (filter_out (null o cancel_now));
   1.165          broadcast_work ());
   1.166  
   1.167  
   1.168 @@ -388,12 +402,15 @@
   1.169  
   1.170  (** futures **)
   1.171  
   1.172 -(* cancellation *)
   1.173 +(* cancel *)
   1.174  
   1.175 -(*cancel: present and future group members will be interrupted eventually*)
   1.176 -fun cancel_group group = SYNCHRONIZED "cancel" (fn () =>
   1.177 - (if cancel_now group then () else cancel_later group;
   1.178 -  signal work_available; scheduler_check ()));
   1.179 +fun cancel_group group = SYNCHRONIZED "cancel_group" (fn () =>
   1.180 +  let
   1.181 +    val running = cancel_now group;
   1.182 +    val _ =
   1.183 +      if null running then ()
   1.184 +      else (cancel_later group; signal work_available; scheduler_check ());
   1.185 +  in running end);
   1.186  
   1.187  fun cancel x = cancel_group (Task_Queue.group_of_task (task_of x));
   1.188  
   1.189 @@ -430,8 +447,7 @@
   1.190                Multithreading.with_attributes
   1.191                  (if interrupts
   1.192                   then Multithreading.private_interrupts else Multithreading.no_interrupts)
   1.193 -                (fn _ => Position.setmp_thread_data pos e ()) before
   1.194 -              Multithreading.interrupted ()) ()
   1.195 +                (fn _ => Position.setmp_thread_data pos e ())) ()
   1.196            else Exn.interrupt_exn;
   1.197        in assign_result group result res end;
   1.198    in (result, job) end;
   1.199 @@ -440,8 +456,7 @@
   1.200  (* fork *)
   1.201  
   1.202  type fork_params =
   1.203 - {name: string, group: Task_Queue.group option, deps: Task_Queue.task list,
   1.204 -  pri: int, interrupts: bool};
   1.205 +  {name: string, group: group option, deps: task list, pri: int, interrupts: bool};
   1.206  
   1.207  fun forks ({name, group, deps, pri, interrupts}: fork_params) es =
   1.208    if null es then []
   1.209 @@ -469,7 +484,7 @@
   1.210      end;
   1.211  
   1.212  fun fork_pri pri e =
   1.213 -  singleton (forks {name = "", group = NONE, deps = [], pri = pri, interrupts = true}) e;
   1.214 +  (singleton o forks) {name = "fork", group = NONE, deps = [], pri = pri, interrupts = true} e;
   1.215  
   1.216  fun fork e = fork_pri 0 e;
   1.217  
   1.218 @@ -521,21 +536,30 @@
   1.219  fun join_result x = singleton join_results x;
   1.220  fun join x = Exn.release (join_result x);
   1.221  
   1.222 +fun join_tasks [] = ()
   1.223 +  | join_tasks tasks =
   1.224 +      (singleton o forks)
   1.225 +        {name = "join_tasks", group = SOME (new_group NONE),
   1.226 +          deps = tasks, pri = 0, interrupts = false} I
   1.227 +      |> join;
   1.228 +
   1.229  
   1.230  (* fast-path versions -- bypassing task queue *)
   1.231  
   1.232 -fun value (x: 'a) =
   1.233 +fun value_result (res: 'a Exn.result) =
   1.234    let
   1.235      val task = Task_Queue.dummy_task ();
   1.236      val group = Task_Queue.group_of_task task;
   1.237      val result = Single_Assignment.var "value" : 'a result;
   1.238 -    val _ = assign_result group result (Exn.Res x);
   1.239 +    val _ = assign_result group result res;
   1.240    in Future {promised = false, task = task, result = result} end;
   1.241  
   1.242 +fun value x = value_result (Exn.Res x);
   1.243 +
   1.244  fun map_future f x =
   1.245    let
   1.246      val task = task_of x;
   1.247 -    val group = Task_Queue.new_group (SOME (Task_Queue.group_of_task task));
   1.248 +    val group = new_group (SOME (Task_Queue.group_of_task task));
   1.249      val (result, job) = future_job group true (fn () => f (join x));
   1.250  
   1.251      val extended = SYNCHRONIZED "extend" (fn () =>
   1.252 @@ -545,32 +569,36 @@
   1.253    in
   1.254      if extended then Future {promised = false, task = task, result = result}
   1.255      else
   1.256 -      singleton
   1.257 -        (forks {name = "Future.map", group = SOME group, deps = [task],
   1.258 -          pri = Task_Queue.pri_of_task task, interrupts = true})
   1.259 +      (singleton o forks)
   1.260 +        {name = "map_future", group = SOME group, deps = [task],
   1.261 +          pri = Task_Queue.pri_of_task task, interrupts = true}
   1.262          (fn () => f (join x))
   1.263    end;
   1.264  
   1.265  fun cond_forks args es =
   1.266    if Multithreading.enabled () then forks args es
   1.267 -  else map (fn e => value (e ())) es;
   1.268 +  else map (fn e => value_result (Exn.interruptible_capture e ())) es;
   1.269  
   1.270  
   1.271  (* promised futures -- fulfilled by external means *)
   1.272  
   1.273 -fun promise_group group : 'a future =
   1.274 +fun promise_group group abort : 'a future =
   1.275    let
   1.276      val result = Single_Assignment.var "promise" : 'a result;
   1.277 -    fun abort () = assign_result group result Exn.interrupt_exn
   1.278 +    fun assign () = assign_result group result Exn.interrupt_exn
   1.279        handle Fail _ => true
   1.280          | exn =>
   1.281 -            if Exn.is_interrupt exn then raise Fail "Concurrent attempt to fulfill promise"
   1.282 +            if Exn.is_interrupt exn
   1.283 +            then raise Fail "Concurrent attempt to fulfill promise"
   1.284              else reraise exn;
   1.285 +    fun job () =
   1.286 +      Multithreading.with_attributes Multithreading.no_interrupts
   1.287 +        (fn _ => assign () before abort ());
   1.288      val task = SYNCHRONIZED "enqueue_passive" (fn () =>
   1.289 -      Unsynchronized.change_result queue (Task_Queue.enqueue_passive group abort));
   1.290 +      Unsynchronized.change_result queue (Task_Queue.enqueue_passive group job));
   1.291    in Future {promised = true, task = task, result = result} end;
   1.292  
   1.293 -fun promise () = promise_group (worker_subgroup ());
   1.294 +fun promise abort = promise_group (worker_subgroup ()) abort;
   1.295  
   1.296  fun fulfill_result (Future {promised, task, result}) res =
   1.297    if not promised then raise Fail "Not a promised future"
     2.1 --- a/src/Pure/Concurrent/lazy.ML	Fri Aug 19 15:54:43 2011 -0700
     2.2 +++ b/src/Pure/Concurrent/lazy.ML	Fri Aug 19 16:55:43 2011 -0700
     2.3 @@ -57,7 +57,7 @@
     2.4            val (expr, x) =
     2.5              Synchronized.change_result var
     2.6                (fn Expr e =>
     2.7 -                    let val x = Future.promise ()
     2.8 +                    let val x = Future.promise I
     2.9                      in ((SOME e, x), Result x) end
    2.10                  | Result x => ((NONE, x), Result x));
    2.11          in
     3.1 --- a/src/Pure/Concurrent/par_exn.ML	Fri Aug 19 15:54:43 2011 -0700
     3.2 +++ b/src/Pure/Concurrent/par_exn.ML	Fri Aug 19 16:55:43 2011 -0700
     3.3 @@ -22,7 +22,11 @@
     3.4  fun serial exn =
     3.5    (case get_exn_serial exn of
     3.6      SOME i => (i, exn)
     3.7 -  | NONE => let val i = Library.serial () in (i, set_exn_serial i exn) end);
     3.8 +  | NONE =>
     3.9 +      let
    3.10 +        val i = Library.serial ();
    3.11 +        val exn' = uninterruptible (fn _ => set_exn_serial i) exn;
    3.12 +      in (i, exn') end);
    3.13  
    3.14  val the_serial = the o get_exn_serial;
    3.15  
     4.1 --- a/src/Pure/Concurrent/par_list.ML	Fri Aug 19 15:54:43 2011 -0700
     4.2 +++ b/src/Pure/Concurrent/par_list.ML	Fri Aug 19 16:55:43 2011 -0700
     4.3 @@ -34,12 +34,13 @@
     4.4    then map (Exn.capture f) xs
     4.5    else
     4.6      let
     4.7 -      val group = Task_Queue.new_group (Future.worker_group ());
     4.8 +      val group = Future.new_group (Future.worker_group ());
     4.9        val futures =
    4.10          Future.forks {name = name, group = SOME group, deps = [], pri = 0, interrupts = true}
    4.11            (map (fn x => fn () => f x) xs);
    4.12        val results = Future.join_results futures
    4.13 -        handle exn => (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn);
    4.14 +        handle exn =>
    4.15 +          (if Exn.is_interrupt exn then ignore (Future.cancel_group group) else (); reraise exn);
    4.16      in results end;
    4.17  
    4.18  fun map_name name f xs = Par_Exn.release_first (managed_results name f xs);
     5.1 --- a/src/Pure/Concurrent/task_queue.ML	Fri Aug 19 15:54:43 2011 -0700
     5.2 +++ b/src/Pure/Concurrent/task_queue.ML	Fri Aug 19 16:55:43 2011 -0700
     5.3 @@ -31,7 +31,7 @@
     5.4    val known_task: queue -> task -> bool
     5.5    val all_passive: queue -> bool
     5.6    val status: queue -> {ready: int, pending: int, running: int, passive: int}
     5.7 -  val cancel: queue -> group -> bool
     5.8 +  val cancel: queue -> group -> task list
     5.9    val cancel_all: queue -> group list
    5.10    val finish: task -> queue -> bool * queue
    5.11    val enqueue_passive: group -> (unit -> bool) -> queue -> task * queue
    5.12 @@ -248,10 +248,12 @@
    5.13    let
    5.14      val _ = cancel_group group Exn.Interrupt;
    5.15      val running =
    5.16 -      Tasks.fold (#1 #> get_job jobs #> (fn Running t => insert Thread.equal t | _ => I))
    5.17 +      Tasks.fold (fn (task, _) =>
    5.18 +          (case get_job jobs task of Running thread => cons (task, thread) | _ => I))
    5.19          (get_tasks groups (group_id group)) [];
    5.20 -    val _ = List.app Simple_Thread.interrupt_unsynchronized running;
    5.21 -  in null running end;
    5.22 +    val threads = fold (insert Thread.equal o #2) running [];
    5.23 +    val _ = List.app Simple_Thread.interrupt_unsynchronized threads;
    5.24 +  in map #1 running end;
    5.25  
    5.26  fun cancel_all (Queue {jobs, ...}) =
    5.27    let
     6.1 --- a/src/Pure/General/markup.ML	Fri Aug 19 15:54:43 2011 -0700
     6.2 +++ b/src/Pure/General/markup.ML	Fri Aug 19 16:55:43 2011 -0700
     6.3 @@ -119,6 +119,7 @@
     6.4    val badN: string val bad: T
     6.5    val functionN: string
     6.6    val invoke_scala: string -> string -> Properties.T
     6.7 +  val cancel_scala: string -> Properties.T
     6.8    val no_output: Output.output * Output.output
     6.9    val default_output: T -> Output.output * Output.output
    6.10    val add_mode: string -> (T -> Output.output * Output.output) -> unit
    6.11 @@ -377,6 +378,7 @@
    6.12  val functionN = "function"
    6.13  
    6.14  fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
    6.15 +fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
    6.16  
    6.17  
    6.18  
     7.1 --- a/src/Pure/General/markup.scala	Fri Aug 19 15:54:43 2011 -0700
     7.2 +++ b/src/Pure/General/markup.scala	Fri Aug 19 16:55:43 2011 -0700
     7.3 @@ -283,6 +283,16 @@
     7.4        }
     7.5    }
     7.6  
     7.7 +  val CANCEL_SCALA = "cancel_scala"
     7.8 +  object Cancel_Scala
     7.9 +  {
    7.10 +    def unapply(props: Properties.T): Option[String] =
    7.11 +      props match {
    7.12 +        case List((FUNCTION, CANCEL_SCALA), (ID, id)) => Some(id)
    7.13 +        case _ => None
    7.14 +      }
    7.15 +  }
    7.16 +
    7.17  
    7.18    /* system data */
    7.19  
     8.1 --- a/src/Pure/Isar/runtime.ML	Fri Aug 19 15:54:43 2011 -0700
     8.2 +++ b/src/Pure/Isar/runtime.ML	Fri Aug 19 16:55:43 2011 -0700
     8.3 @@ -119,7 +119,7 @@
     8.4    else f x;
     8.5  
     8.6  fun controlled_execution f x =
     8.7 -  ((f |> debugging |> Future.interruptible_task) x before Multithreading.interrupted ());
     8.8 +  (f |> debugging |> Future.interruptible_task) x;
     8.9  
    8.10  fun toplevel_error output_exn f x = f x
    8.11    handle exn =>
     9.1 --- a/src/Pure/Isar/toplevel.ML	Fri Aug 19 15:54:43 2011 -0700
     9.2 +++ b/src/Pure/Isar/toplevel.ML	Fri Aug 19 16:55:43 2011 -0700
     9.3 @@ -419,6 +419,14 @@
     9.4  
     9.5  (* theory transitions *)
     9.6  
     9.7 +val global_theory_group =
     9.8 +  Sign.new_group #>
     9.9 +  Global_Theory.begin_recent_proofs #> Theory.checkpoint;
    9.10 +
    9.11 +val local_theory_group =
    9.12 +  Local_Theory.new_group #>
    9.13 +  Local_Theory.raw_theory (Global_Theory.begin_recent_proofs #> Theory.checkpoint);
    9.14 +
    9.15  fun generic_theory f = transaction (fn _ =>
    9.16    (fn Theory (gthy, _) => Theory (f gthy, NONE)
    9.17      | _ => raise UNDEF));
    9.18 @@ -426,8 +434,7 @@
    9.19  fun theory' f = transaction (fn int =>
    9.20    (fn Theory (Context.Theory thy, _) =>
    9.21        let val thy' = thy
    9.22 -        |> Sign.new_group
    9.23 -        |> Theory.checkpoint
    9.24 +        |> global_theory_group
    9.25          |> f int
    9.26          |> Sign.reset_group;
    9.27        in Theory (Context.Theory thy', NONE) end
    9.28 @@ -454,7 +461,7 @@
    9.29          let
    9.30            val finish = loc_finish loc gthy;
    9.31            val lthy' = loc_begin loc gthy
    9.32 -            |> Local_Theory.new_group
    9.33 +            |> local_theory_group
    9.34              |> f int
    9.35              |> Local_Theory.reset_group;
    9.36          in Theory (finish lthy', SOME lthy') end
    9.37 @@ -506,13 +513,13 @@
    9.38  in
    9.39  
    9.40  fun local_theory_to_proof' loc f = begin_proof
    9.41 -  (fn int => fn gthy => f int (Local_Theory.new_group (loc_begin loc gthy)))
    9.42 +  (fn int => fn gthy => f int (local_theory_group (loc_begin loc gthy)))
    9.43    (fn gthy => loc_finish loc gthy o Local_Theory.reset_group);
    9.44  
    9.45  fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f);
    9.46  
    9.47  fun theory_to_proof f = begin_proof
    9.48 -  (K (fn Context.Theory thy => f (Theory.checkpoint (Sign.new_group thy)) | _ => raise UNDEF))
    9.49 +  (K (fn Context.Theory thy => f (global_theory_group thy) | _ => raise UNDEF))
    9.50    (K (Context.Theory o Sign.reset_group o Proof_Context.theory_of));
    9.51  
    9.52  end;
    10.1 --- a/src/Pure/PIDE/document.ML	Fri Aug 19 15:54:43 2011 -0700
    10.2 +++ b/src/Pure/PIDE/document.ML	Fri Aug 19 16:55:43 2011 -0700
    10.3 @@ -24,7 +24,7 @@
    10.4    type state
    10.5    val init_state: state
    10.6    val join_commands: state -> unit
    10.7 -  val cancel_execution: state -> unit -> unit
    10.8 +  val cancel_execution: state -> Future.task list
    10.9    val define_command: command_id -> string -> state -> state
   10.10    val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
   10.11    val execute: version_id -> state -> state
   10.12 @@ -164,7 +164,7 @@
   10.13   {versions: version Inttab.table,  (*version_id -> document content*)
   10.14    commands: Toplevel.transition future Inttab.table,  (*command_id -> transition (future parsing)*)
   10.15    execs: Toplevel.state lazy Inttab.table,  (*exec_id -> execution process*)
   10.16 -  execution: unit future list}  (*global execution process*)
   10.17 +  execution: Future.group}  (*global execution process*)
   10.18  with
   10.19  
   10.20  fun make_state (versions, commands, execs, execution) =
   10.21 @@ -177,7 +177,7 @@
   10.22    make_state (Inttab.make [(no_id, empty_version)],
   10.23      Inttab.make [(no_id, Future.value Toplevel.empty)],
   10.24      Inttab.make [(no_id, empty_exec)],
   10.25 -    []);
   10.26 +    Future.new_group NONE);
   10.27  
   10.28  
   10.29  (* document versions *)
   10.30 @@ -200,9 +200,10 @@
   10.31    map_state (fn (versions, commands, execs, execution) =>
   10.32      let
   10.33        val id_string = print_id id;
   10.34 -      val tr = Future.fork_pri 2 (fn () =>
   10.35 -        Position.setmp_thread_data (Position.id_only id_string)
   10.36 -          (fn () => Outer_Syntax.prepare_command (Position.id id_string) text) ());
   10.37 +      val tr =
   10.38 +        Future.fork_pri 2 (fn () =>
   10.39 +          Position.setmp_thread_data (Position.id_only id_string)
   10.40 +            (fn () => Outer_Syntax.prepare_command (Position.id id_string) text) ());
   10.41        val commands' =
   10.42          Inttab.update_new (id, tr) commands
   10.43            handle Inttab.DUP dup => err_dup "command" dup;
   10.44 @@ -233,9 +234,7 @@
   10.45  
   10.46  (* document execution *)
   10.47  
   10.48 -fun cancel_execution (State {execution, ...}) =
   10.49 -  (List.app Future.cancel execution;
   10.50 -    fn () => ignore (Future.join_results execution));
   10.51 +fun cancel_execution (State {execution, ...}) = Future.cancel_group execution;
   10.52  
   10.53  end;
   10.54  
   10.55 @@ -253,13 +252,13 @@
   10.56    | NONE => ());
   10.57  
   10.58  fun async_state tr st =
   10.59 -  ignore
   10.60 -    (singleton
   10.61 -      (Future.forks {name = "Document.async_state",
   10.62 -        group = SOME (Task_Queue.new_group NONE), deps = [], pri = 0, interrupts = true})
   10.63 -      (fn () =>
   10.64 -        Toplevel.setmp_thread_position tr
   10.65 -          (fn () => Toplevel.print_state false st) ()));
   10.66 +  (singleton o Future.forks)
   10.67 +    {name = "Document.async_state", group = SOME (Future.new_group NONE),
   10.68 +      deps = [], pri = 0, interrupts = true}
   10.69 +    (fn () =>
   10.70 +      Toplevel.setmp_thread_position tr
   10.71 +        (fn () => Toplevel.print_state false st) ())
   10.72 +  |> ignore;
   10.73  
   10.74  fun run int tr st =
   10.75    (case Toplevel.transition int tr st of
   10.76 @@ -355,9 +354,9 @@
   10.77                  fun get_command id =
   10.78                    (id, the_command state id |> Future.map (Toplevel.modify_init init));
   10.79                in
   10.80 -                singleton
   10.81 -                  (Future.forks {name = "Document.edit", group = NONE,
   10.82 -                    deps = map (Future.task_of o #2) deps, pri = 2, interrupts = false})
   10.83 +                (singleton o Future.forks)
   10.84 +                  {name = "Document.edit", group = NONE,
   10.85 +                    deps = map (Future.task_of o #2) deps, pri = 2, interrupts = false}
   10.86                    (fn () =>
   10.87                      let
   10.88                        val prev_exec =
   10.89 @@ -393,17 +392,16 @@
   10.90        fun force_exec NONE = ()
   10.91          | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
   10.92  
   10.93 -      val execution' =
   10.94 +      val execution = Future.new_group NONE;
   10.95 +      val _ =
   10.96          nodes_of version |> Graph.schedule
   10.97            (fn deps => fn (name, node) =>
   10.98 -            singleton
   10.99 -              (Future.forks
  10.100 -                {name = "theory:" ^ name, group = NONE,
  10.101 -                  deps = map (Future.task_of o #2) deps,
  10.102 -                  pri = 1, interrupts = true})
  10.103 +            (singleton o Future.forks)
  10.104 +              {name = "theory:" ^ name, group = SOME (Future.new_group (SOME execution)),
  10.105 +                deps = map (Future.task_of o #2) deps, pri = 1, interrupts = true}
  10.106                (fold_entries NONE (fn (_, exec) => fn () => force_exec exec) node));
  10.107  
  10.108 -    in (versions, commands, execs, execution') end);
  10.109 +    in (versions, commands, execs, execution) end);
  10.110  
  10.111  
  10.112  
    11.1 --- a/src/Pure/PIDE/isar_document.ML	Fri Aug 19 15:54:43 2011 -0700
    11.2 +++ b/src/Pure/PIDE/isar_document.ML	Fri Aug 19 16:55:43 2011 -0700
    11.3 @@ -30,9 +30,9 @@
    11.4                    fn ([a], []) => Document.Header (Exn.Exn (ERROR a))]))
    11.5              end;
    11.6  
    11.7 -      val await_cancellation = Document.cancel_execution state;
    11.8 +      val running = Document.cancel_execution state;
    11.9        val (updates, state') = Document.edit old_id new_id edits state;
   11.10 -      val _ = await_cancellation ();
   11.11 +      val _ = Future.join_tasks running;
   11.12        val _ = Document.join_commands state';
   11.13        val _ =
   11.14          Output.status (Markup.markup (Markup.assign new_id)
    12.1 --- a/src/Pure/System/invoke_scala.ML	Fri Aug 19 15:54:43 2011 -0700
    12.2 +++ b/src/Pure/System/invoke_scala.ML	Fri Aug 19 16:55:43 2011 -0700
    12.3 @@ -33,7 +33,8 @@
    12.4  fun promise_method name arg =
    12.5    let
    12.6      val id = new_id ();
    12.7 -    val promise = Future.promise () : string future;
    12.8 +    fun abort () = Output.raw_message (Markup.cancel_scala id) "";
    12.9 +    val promise = Future.promise abort : string future;
   12.10      val _ = Synchronized.change promises (Symtab.update (id, promise));
   12.11      val _ = Output.raw_message (Markup.invoke_scala name id) arg;
   12.12    in promise end;
    13.1 --- a/src/Pure/System/session.scala	Fri Aug 19 15:54:43 2011 -0700
    13.2 +++ b/src/Pure/System/session.scala	Fri Aug 19 16:55:43 2011 -0700
    13.3 @@ -275,6 +275,8 @@
    13.4              val (tag, res) = Invoke_Scala.method(name, arg)
    13.5              prover.get.invoke_scala(id, tag, res)
    13.6            }
    13.7 +        case Markup.Cancel_Scala(id) =>
    13.8 +          System.err.println("cancel_scala " + id)  // FIXME cancel JVM task
    13.9          case _ =>
   13.10            if (result.is_syslog) {
   13.11              reverse_syslog ::= result.message
    14.1 --- a/src/Pure/Thy/thy_info.ML	Fri Aug 19 15:54:43 2011 -0700
    14.2 +++ b/src/Pure/Thy/thy_info.ML	Fri Aug 19 16:55:43 2011 -0700
    14.3 @@ -194,11 +194,9 @@
    14.4    Graph.schedule (fn deps => fn (name, task) =>
    14.5      (case task of
    14.6        Task (parents, body) =>
    14.7 -        singleton
    14.8 -          (Future.forks
    14.9 -            {name = "theory:" ^ name, group = NONE,
   14.10 -              deps = map (Future.task_of o #2) deps,
   14.11 -              pri = 0, interrupts = true})
   14.12 +        (singleton o Future.forks)
   14.13 +          {name = "theory:" ^ name, group = NONE,
   14.14 +            deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true}
   14.15            (fn () =>
   14.16              (case filter (not o can Future.join o #2) deps of
   14.17                [] => body (map (#1 o Future.join) (task_parents deps parents))
    15.1 --- a/src/Pure/global_theory.ML	Fri Aug 19 15:54:43 2011 -0700
    15.2 +++ b/src/Pure/global_theory.ML	Fri Aug 19 16:55:43 2011 -0700
    15.3 @@ -10,6 +10,8 @@
    15.4    val intern_fact: theory -> xstring -> string
    15.5    val defined_fact: theory -> string -> bool
    15.6    val hide_fact: bool -> string -> theory -> theory
    15.7 +  val begin_recent_proofs: theory -> theory
    15.8 +  val join_recent_proofs: theory -> unit
    15.9    val join_proofs: theory -> unit
   15.10    val get_fact: Context.generic -> theory -> Facts.ref -> thm list
   15.11    val get_thms: theory -> xstring -> thm list
   15.12 @@ -49,10 +51,10 @@
   15.13  
   15.14  structure Data = Theory_Data
   15.15  (
   15.16 -  type T = Facts.T * thm list;
   15.17 -  val empty = (Facts.empty, []);
   15.18 -  fun extend (facts, _) = (facts, []);
   15.19 -  fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), []);
   15.20 +  type T = Facts.T * (thm list * thm list);
   15.21 +  val empty = (Facts.empty, ([], []));
   15.22 +  fun extend (facts, _) = (facts, ([], []));
   15.23 +  fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), ([], []));
   15.24  );
   15.25  
   15.26  
   15.27 @@ -68,10 +70,11 @@
   15.28  
   15.29  (* proofs *)
   15.30  
   15.31 -fun register_proofs (thy, thms) = (Data.map (apsnd (append thms)) thy, thms);
   15.32 +fun register_proofs (thy, thms) = (Data.map (apsnd (pairself (append thms))) thy, thms);
   15.33  
   15.34 -fun join_proofs thy = Thm.join_proofs (rev (#2 (Data.get thy)));
   15.35 -
   15.36 +val begin_recent_proofs = Data.map (apsnd (fn (_, thms) => ([], thms)));
   15.37 +val join_recent_proofs = Thm.join_proofs o rev o #1 o #2 o Data.get;
   15.38 +val join_proofs = Thm.join_proofs o rev o #2 o #2 o Data.get;
   15.39  
   15.40  
   15.41  (** retrieve theorems **)
    16.1 --- a/src/Pure/goal.ML	Fri Aug 19 15:54:43 2011 -0700
    16.2 +++ b/src/Pure/goal.ML	Fri Aug 19 16:55:43 2011 -0700
    16.3 @@ -124,8 +124,8 @@
    16.4      let
    16.5        val _ = forked 1;
    16.6        val future =
    16.7 -        singleton
    16.8 -          (Future.forks {name = name, group = NONE, deps = [], pri = ~1, interrupts = false})
    16.9 +        (singleton o Future.forks)
   16.10 +          {name = name, group = NONE, deps = [], pri = ~1, interrupts = false}
   16.11            (fn () =>
   16.12              Exn.release
   16.13                (Exn.capture (Future.status o Future.interruptible_task) e before forked ~1));
    17.1 --- a/src/Pure/proofterm.ML	Fri Aug 19 15:54:43 2011 -0700
    17.2 +++ b/src/Pure/proofterm.ML	Fri Aug 19 16:55:43 2011 -0700
    17.3 @@ -37,11 +37,11 @@
    17.4  
    17.5    type oracle = string * term
    17.6    type pthm = serial * (string * term * proof_body future)
    17.7 +  val join_body: proof_body -> unit
    17.8    val proof_of: proof_body -> proof
    17.9    val join_proof: proof_body future -> proof
   17.10    val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
   17.11    val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
   17.12 -  val join_bodies: proof_body list -> unit
   17.13    val status_of: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
   17.14  
   17.15    val oracle_ord: oracle * oracle -> order
   17.16 @@ -171,6 +171,10 @@
   17.17  type oracle = string * term;
   17.18  type pthm = serial * (string * term * proof_body future);
   17.19  
   17.20 +fun join_thm (pthm: pthm) = ignore (Future.join (#3 (#2 pthm)));
   17.21 +fun join_thms thms = (Future.join_results (map (#3 o #2) thms); List.app join_thm thms);
   17.22 +fun join_body (PBody {thms, ...}) = join_thms thms;
   17.23 +
   17.24  fun proof_of (PBody {proof, ...}) = proof;
   17.25  val join_proof = Future.join #> proof_of;
   17.26  
   17.27 @@ -195,18 +199,15 @@
   17.28  fun fold_body_thms f =
   17.29    let
   17.30      fun app (PBody {thms, ...}) =
   17.31 -     (Future.join_results (map (#3 o #2) thms);
   17.32 -      thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
   17.33 +      tap join_thms thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
   17.34          if Inttab.defined seen i then (x, seen)
   17.35          else
   17.36            let
   17.37              val body' = Future.join body;
   17.38              val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
   17.39 -          in (f (name, prop, body') x', seen') end));
   17.40 +          in (f (name, prop, body') x', seen') end);
   17.41    in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
   17.42  
   17.43 -fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies ();
   17.44 -
   17.45  fun status_of bodies =
   17.46    let
   17.47      fun status (PBody {oracles, thms, ...}) x =
   17.48 @@ -242,14 +243,13 @@
   17.49  val all_oracles_of =
   17.50    let
   17.51      fun collect (PBody {oracles, thms, ...}) =
   17.52 -     (Future.join_results (map (#3 o #2) thms);
   17.53 -      thms |> fold (fn (i, (_, _, body)) => fn (x, seen) =>
   17.54 +      tap join_thms thms |> fold (fn (i, (_, _, body)) => fn (x, seen) =>
   17.55          if Inttab.defined seen i then (x, seen)
   17.56          else
   17.57            let
   17.58              val body' = Future.join body;
   17.59              val (x', seen') = collect body' (x, Inttab.update (i, ()) seen);
   17.60 -          in (merge_oracles oracles x', seen') end));
   17.61 +          in (merge_oracles oracles x', seen') end);
   17.62    in fn body => #1 (collect body ([], Inttab.empty)) end;
   17.63  
   17.64  fun approximate_proof_body prf =
   17.65 @@ -1396,16 +1396,17 @@
   17.66        | fill _ = NONE;
   17.67      val (rules, procs) = get_data thy;
   17.68      val proof = rewrite_prf fst (rules, K (K fill) :: procs) proof0;
   17.69 +    val _ = join_thms thms;
   17.70    in PBody {oracles = oracles, thms = thms, proof = proof} end;
   17.71  
   17.72  fun fulfill_proof_future _ [] postproc body =
   17.73        if not (Multithreading.enabled ()) then Future.value (postproc (Future.join body))
   17.74        else Future.map postproc body
   17.75    | fulfill_proof_future thy promises postproc body =
   17.76 -      singleton
   17.77 -        (Future.forks {name = "Proofterm.fulfill_proof_future", group = NONE,
   17.78 -            deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0,
   17.79 -            interrupts = true})
   17.80 +      (singleton o Future.forks)
   17.81 +        {name = "Proofterm.fulfill_proof_future", group = NONE,
   17.82 +          deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0,
   17.83 +          interrupts = true}
   17.84          (fn () =>
   17.85            postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body)));
   17.86  
   17.87 @@ -1461,10 +1462,9 @@
   17.88        if not (proofs_enabled ()) then Future.value (make_body0 MinProof)
   17.89        else if not (Multithreading.enabled ()) then Future.value (make_body0 (full_proof0 ()))
   17.90        else
   17.91 -        singleton
   17.92 -          (Future.forks
   17.93 -            {name = "Proofterm.prepare_thm_proof", group = NONE, deps = [], pri = ~1,
   17.94 -              interrupts = true})
   17.95 +        (singleton o Future.forks)
   17.96 +          {name = "Proofterm.prepare_thm_proof", group = NONE,
   17.97 +            deps = [], pri = ~1, interrupts = true}
   17.98            (make_body0 o full_proof0);
   17.99  
  17.100      fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);
    18.1 --- a/src/Pure/thm.ML	Fri Aug 19 15:54:43 2011 -0700
    18.2 +++ b/src/Pure/thm.ML	Fri Aug 19 16:55:43 2011 -0700
    18.3 @@ -517,9 +517,9 @@
    18.4      (map #1 promises ~~ fulfill_bodies (map #2 promises)) body
    18.5  and fulfill_bodies futures = map fulfill_body (Par_Exn.release_all (Future.join_results futures));
    18.6  
    18.7 -val join_proofs = Proofterm.join_bodies o map fulfill_body;
    18.8 +fun join_proofs thms = ignore (map fulfill_body thms);
    18.9  
   18.10 -fun proof_body_of thm = (Proofterm.join_bodies [raw_body thm]; fulfill_body thm);
   18.11 +fun proof_body_of thm = (Proofterm.join_body (raw_body thm); fulfill_body thm);
   18.12  val proof_of = Proofterm.proof_of o proof_body_of;
   18.13  
   18.14  
    19.1 --- a/src/Tools/jEdit/src/raw_output_dockable.scala	Fri Aug 19 15:54:43 2011 -0700
    19.2 +++ b/src/Tools/jEdit/src/raw_output_dockable.scala	Fri Aug 19 16:55:43 2011 -0700
    19.3 @@ -21,7 +21,6 @@
    19.4    extends Dockable(view: View, position: String)
    19.5  {
    19.6    private val text_area = new TextArea
    19.7 -  text_area.editable = false
    19.8    set_content(new ScrollPane(text_area))
    19.9  
   19.10  
    20.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Fri Aug 19 15:54:43 2011 -0700
    20.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Fri Aug 19 16:55:43 2011 -0700
    20.3 @@ -28,7 +28,6 @@
    20.4    readme.render_document(Isabelle_System.try_read(List(Path.explode("$JEDIT_HOME/README.html"))))
    20.5  
    20.6    private val syslog = new TextArea(Isabelle.session.syslog())
    20.7 -  syslog.editable = false
    20.8  
    20.9    private val tabs = new TabbedPane {
   20.10      pages += new TabbedPane.Page("README", Component.wrap(readme))