1.1 --- a/src/Pure/Concurrent/future.ML Fri Aug 19 10:46:54 2011 -0700
1.2 +++ b/src/Pure/Concurrent/future.ML Fri Aug 19 23:48:18 2011 +0200
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 10:46:54 2011 -0700
2.2 +++ b/src/Pure/Concurrent/lazy.ML Fri Aug 19 23:48:18 2011 +0200
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 10:46:54 2011 -0700
3.2 +++ b/src/Pure/Concurrent/par_exn.ML Fri Aug 19 23:48:18 2011 +0200
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 10:46:54 2011 -0700
4.2 +++ b/src/Pure/Concurrent/par_list.ML Fri Aug 19 23:48:18 2011 +0200
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 10:46:54 2011 -0700
5.2 +++ b/src/Pure/Concurrent/task_queue.ML Fri Aug 19 23:48:18 2011 +0200
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 10:46:54 2011 -0700
6.2 +++ b/src/Pure/General/markup.ML Fri Aug 19 23:48:18 2011 +0200
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 10:46:54 2011 -0700
7.2 +++ b/src/Pure/General/markup.scala Fri Aug 19 23:48:18 2011 +0200
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 10:46:54 2011 -0700
8.2 +++ b/src/Pure/Isar/runtime.ML Fri Aug 19 23:48:18 2011 +0200
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 10:46:54 2011 -0700
9.2 +++ b/src/Pure/Isar/toplevel.ML Fri Aug 19 23:48:18 2011 +0200
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 10:46:54 2011 -0700
10.2 +++ b/src/Pure/PIDE/document.ML Fri Aug 19 23:48:18 2011 +0200
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 10:46:54 2011 -0700
11.2 +++ b/src/Pure/PIDE/isar_document.ML Fri Aug 19 23:48:18 2011 +0200
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 10:46:54 2011 -0700
12.2 +++ b/src/Pure/System/invoke_scala.ML Fri Aug 19 23:48:18 2011 +0200
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 10:46:54 2011 -0700
13.2 +++ b/src/Pure/System/session.scala Fri Aug 19 23:48:18 2011 +0200
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 10:46:54 2011 -0700
14.2 +++ b/src/Pure/Thy/thy_info.ML Fri Aug 19 23:48:18 2011 +0200
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 10:46:54 2011 -0700
15.2 +++ b/src/Pure/global_theory.ML Fri Aug 19 23:48:18 2011 +0200
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 10:46:54 2011 -0700
16.2 +++ b/src/Pure/goal.ML Fri Aug 19 23:48:18 2011 +0200
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 10:46:54 2011 -0700
17.2 +++ b/src/Pure/proofterm.ML Fri Aug 19 23:48:18 2011 +0200
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 10:46:54 2011 -0700
18.2 +++ b/src/Pure/thm.ML Fri Aug 19 23:48:18 2011 +0200
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 10:46:54 2011 -0700
19.2 +++ b/src/Tools/jEdit/src/raw_output_dockable.scala Fri Aug 19 23:48:18 2011 +0200
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 10:46:54 2011 -0700
20.2 +++ b/src/Tools/jEdit/src/session_dockable.scala Fri Aug 19 23:48:18 2011 +0200
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))