more abstract Future.is_worker;
Future.fork_local: inherit from worker (if available);
--- a/src/Pure/Concurrent/future.ML Sun Jul 19 17:08:34 2009 +0200
+++ b/src/Pure/Concurrent/future.ML Sun Jul 19 18:02:40 2009 +0200
@@ -29,7 +29,7 @@
val enabled: unit -> bool
type task = Task_Queue.task
type group = Task_Queue.group
- val thread_data: unit -> (string * task) option
+ val is_worker: unit -> bool
type 'a future
val task_of: 'a future -> task
val group_of: 'a future -> group
@@ -40,6 +40,7 @@
val fork_group: group -> (unit -> 'a) -> 'a future
val fork_deps: 'b future list -> (unit -> 'a) -> 'a future
val fork_pri: int -> (unit -> 'a) -> 'a future
+ val fork_local: int -> (unit -> 'a) -> 'a future
val join_results: 'a future list -> 'a Exn.result list
val join_result: 'a future -> 'a Exn.result
val join: 'a future -> 'a
@@ -66,11 +67,16 @@
type task = Task_Queue.task;
type group = Task_Queue.group;
-local val tag = Universal.tag () : (string * task) option Universal.tag in
+local
+ val tag = Universal.tag () : (string * task * group) option Universal.tag;
+in
fun thread_data () = the_default NONE (Thread.getLocal tag);
- fun setmp_thread_data data f x = Library.setmp_thread_data tag (thread_data ()) (SOME data) f x;
+ fun setmp_thread_data data f x =
+ Library.setmp_thread_data tag (thread_data ()) (SOME data) f x;
end;
+val is_worker = is_some o thread_data;
+
(* datatype future *)
@@ -148,7 +154,7 @@
let
val _ = trace_active ();
val valid = Task_Queue.is_valid group;
- val ok = setmp_thread_data (name, task) (fn () =>
+ val ok = setmp_thread_data (name, task, group) (fn () =>
fold (fn job => fn ok => job valid andalso ok) jobs true) ();
val _ = SYNCHRONIZED "execute" (fn () =>
(change queue (Task_Queue.finish task);
@@ -277,6 +283,7 @@
fun fork_group group e = fork_future (SOME group) [] 0 e;
fun fork_deps deps e = fork_future NONE (map task_of deps) 0 e;
fun fork_pri pri e = fork_future NONE [] pri e;
+fun fork_local pri e = fork_future (Option.map #3 (thread_data ())) [] pri e;
(* join *)
@@ -300,13 +307,13 @@
val _ = Multithreading.self_critical () andalso
error "Cannot join future values within critical section";
- val is_worker = is_some (thread_data ());
+ val worker = is_worker ();
fun join_wait x =
if SYNCHRONIZED "join_wait" (fn () =>
- is_finished x orelse (if is_worker then worker_wait () else wait (); false))
+ is_finished x orelse (if worker then worker_wait () else wait (); false))
then () else join_wait x;
- val _ = if is_worker then join_deps (map task_of xs) else ();
+ val _ = if worker then join_deps (map task_of xs) else ();
val _ = List.app join_wait xs;
in map get_result xs end) ();
@@ -342,7 +349,7 @@
fun interruptible_task f x =
if Multithreading.available then
Multithreading.with_attributes
- (if is_some (thread_data ())
+ (if is_worker ()
then Multithreading.restricted_interrupts
else Multithreading.regular_interrupts)
(fn _ => f) x
--- a/src/Pure/Isar/proof.ML Sun Jul 19 17:08:34 2009 +0200
+++ b/src/Pure/Isar/proof.ML Sun Jul 19 18:02:40 2009 +0200
@@ -1045,7 +1045,7 @@
fun future_terminal_proof proof1 proof2 meths int state =
if int orelse is_relevant state orelse not (Goal.future_enabled ())
then proof1 meths state
- else snd (state |> proof2 (fn state' => Future.fork_pri ~1 (fn () => ((), proof1 meths state'))));
+ else snd (proof2 (fn state' => Future.fork_local ~1 (fn () => ((), proof1 meths state'))) state);
in
--- a/src/Pure/Isar/toplevel.ML Sun Jul 19 17:08:34 2009 +0200
+++ b/src/Pure/Isar/toplevel.ML Sun Jul 19 18:02:40 2009 +0200
@@ -652,7 +652,7 @@
val future_proof = Proof.global_future_proof
(fn prf =>
- Future.fork_pri ~1 (fn () =>
+ Future.fork_local ~1 (fn () =>
let val (states, result_state) =
(case st' of State (SOME (Proof (_, (_, orig_gthy)), exit), prev)
=> State (SOME (Proof (ProofNode.init prf, (finish, orig_gthy)), exit), prev))
--- a/src/Pure/goal.ML Sun Jul 19 17:08:34 2009 +0200
+++ b/src/Pure/goal.ML Sun Jul 19 18:02:40 2009 +0200
@@ -98,7 +98,7 @@
val parallel_proofs = ref true;
fun future_enabled () =
- Future.enabled () andalso ! parallel_proofs andalso is_some (Future.thread_data ());
+ Future.enabled () andalso ! parallel_proofs andalso Future.is_worker ();
(* future_result *)
@@ -185,7 +185,7 @@
val res =
if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse not (future_enabled ())
then result ()
- else future_result ctxt' (Future.fork_pri ~1 result) (Thm.term_of stmt);
+ else future_result ctxt' (Future.fork_local ~1 result) (Thm.term_of stmt);
in
Conjunction.elim_balanced (length props) res
|> map (Assumption.export false ctxt' ctxt)