--- a/src/Pure/Concurrent/future.ML Mon Jan 31 22:57:01 2011 +0100
+++ b/src/Pure/Concurrent/future.ML Mon Jan 31 23:02:53 2011 +0100
@@ -44,7 +44,7 @@
val group_of: 'a future -> group
val peek: 'a future -> 'a Exn.result option
val is_finished: 'a future -> bool
- val bulk: {name: string, group: group option, deps: task list, pri: int} ->
+ val forks: {name: string, group: group option, deps: task list, pri: int} ->
(unit -> 'a) list -> 'a future list
val fork_pri: int -> (unit -> 'a) -> 'a future
val fork: (unit -> 'a) -> 'a future
@@ -400,31 +400,33 @@
(* fork *)
-fun bulk {name, group, deps, pri} es =
- let
- val grp =
- (case group of
- NONE => worker_subgroup ()
- | SOME grp => grp);
- fun enqueue e (minimal, queue) =
- let
- val (result, job) = future_job grp e;
- val ((task, minimal'), queue') = Task_Queue.enqueue name grp deps pri job queue;
- val future = Future {promised = false, task = task, group = grp, result = result};
- in (future, (minimal orelse minimal', queue')) end;
- in
- SYNCHRONIZED "enqueue" (fn () =>
- let
- val (futures, minimal) =
- Unsynchronized.change_result queue (fn q =>
- let val (futures, (minimal, q')) = fold_map enqueue es (false, q)
- in ((futures, minimal), q') end);
- val _ = if minimal then signal work_available else ();
- val _ = scheduler_check ();
- in futures end)
- end;
+fun forks {name, group, deps, pri} es =
+ if null es then []
+ else
+ let
+ val grp =
+ (case group of
+ NONE => worker_subgroup ()
+ | SOME grp => grp);
+ fun enqueue e (minimal, queue) =
+ let
+ val (result, job) = future_job grp e;
+ val ((task, minimal'), queue') = Task_Queue.enqueue name grp deps pri job queue;
+ val future = Future {promised = false, task = task, group = grp, result = result};
+ in (future, (minimal orelse minimal', queue')) end;
+ in
+ SYNCHRONIZED "enqueue" (fn () =>
+ let
+ val (futures, minimal) =
+ Unsynchronized.change_result queue (fn q =>
+ let val (futures, (minimal, q')) = fold_map enqueue es (false, q)
+ in ((futures, minimal), q') end);
+ val _ = if minimal then signal work_available else ();
+ val _ = scheduler_check ();
+ in futures end)
+ end;
-fun fork_pri pri e = singleton (bulk {name = "", group = NONE, deps = [], pri = pri}) e;
+fun fork_pri pri e = singleton (forks {name = "", group = NONE, deps = [], pri = pri}) e;
fun fork e = fork_pri 0 e;
@@ -501,7 +503,7 @@
if extended then Future {promised = false, task = task, group = group, result = result}
else
singleton
- (bulk {name = "Future.map", group = SOME group,
+ (forks {name = "Future.map", group = SOME group,
deps = [task], pri = Task_Queue.pri_of_task task})
(fn () => f (join x))
end;
--- a/src/Pure/Concurrent/par_list.ML Mon Jan 31 22:57:01 2011 +0100
+++ b/src/Pure/Concurrent/par_list.ML Mon Jan 31 23:02:53 2011 +0100
@@ -31,7 +31,7 @@
let
val group = Task_Queue.new_group (Future.worker_group ());
val futures =
- Future.bulk {name = name, group = SOME group, deps = [], pri = 0}
+ Future.forks {name = name, group = SOME group, deps = [], pri = 0}
(map (fn x => fn () => f x) xs);
val results = Future.join_results futures
handle exn => (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn);
--- a/src/Pure/Isar/toplevel.ML Mon Jan 31 22:57:01 2011 +0100
+++ b/src/Pure/Isar/toplevel.ML Mon Jan 31 23:02:53 2011 +0100
@@ -664,7 +664,7 @@
val future_proof = Proof.global_future_proof
(fn prf =>
singleton
- (Future.bulk {name = "Toplevel.proof_result", group = NONE, deps = [], pri = ~1})
+ (Future.forks {name = "Toplevel.proof_result", group = NONE, deps = [], pri = ~1})
(fn () =>
let val (states, result_state) =
(case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
--- a/src/Pure/PIDE/document.ML Mon Jan 31 22:57:01 2011 +0100
+++ b/src/Pure/PIDE/document.ML Mon Jan 31 23:02:53 2011 +0100
@@ -209,7 +209,7 @@
fun async_state tr st =
ignore
(singleton
- (Future.bulk {name = "Document.async_state",
+ (Future.forks {name = "Document.async_state",
group = SOME (Task_Queue.new_group NONE), deps = [], pri = 0})
(fn () =>
Toplevel.setmp_thread_position tr
@@ -339,7 +339,7 @@
val _ = cancel state;
val execution' = (* FIXME proper node deps *)
- Future.bulk {name = "Document.execute", group = NONE, deps = [], pri = 1}
+ Future.forks {name = "Document.execute", group = NONE, deps = [], pri = 1}
[fn () =>
let
val _ = await_cancellation state;
--- a/src/Pure/Thy/thy_info.ML Mon Jan 31 22:57:01 2011 +0100
+++ b/src/Pure/Thy/thy_info.ML Mon Jan 31 23:02:53 2011 +0100
@@ -187,7 +187,7 @@
val future =
singleton
- (Future.bulk {name = "theory " ^ name, group = NONE, deps = task_deps, pri = 0})
+ (Future.forks {name = "theory " ^ name, group = NONE, deps = task_deps, pri = 0})
(fn () =>
(case map_filter failed deps of
[] => body (map (#1 o Future.join o get) parents)
--- a/src/Pure/goal.ML Mon Jan 31 22:57:01 2011 +0100
+++ b/src/Pure/goal.ML Mon Jan 31 23:02:53 2011 +0100
@@ -107,7 +107,7 @@
(* parallel proofs *)
fun fork e =
- singleton (Future.bulk {name = "Goal.fork", group = NONE, deps = [], pri = ~1})
+ singleton (Future.forks {name = "Goal.fork", group = NONE, deps = [], pri = ~1})
(fn () => Future.status e);
val parallel_proofs = Unsynchronized.ref 1;
--- a/src/Pure/proofterm.ML Mon Jan 31 22:57:01 2011 +0100
+++ b/src/Pure/proofterm.ML Mon Jan 31 23:02:53 2011 +0100
@@ -1390,7 +1390,7 @@
else Future.map postproc body
| fulfill_proof_future thy promises postproc body =
singleton
- (Future.bulk {name = "Proofterm.fulfill_proof_future", group = NONE,
+ (Future.forks {name = "Proofterm.fulfill_proof_future", group = NONE,
deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0})
(fn () =>
postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body)));
@@ -1448,7 +1448,7 @@
else if not (Multithreading.enabled ()) then Future.value (make_body0 (full_proof0 ()))
else
singleton
- (Future.bulk {name = "Proofterm.prepare_thm_proof", group = NONE, deps = [], pri = ~1})
+ (Future.forks {name = "Proofterm.prepare_thm_proof", group = NONE, deps = [], pri = ~1})
(make_body0 o full_proof0);
fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);