1.1 --- a/src/Pure/Concurrent/future.ML	Sun Jul 19 17:08:34 2009 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Sun Jul 19 18:02:40 2009 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4    val enabled: unit -> bool
     1.5    type task = Task_Queue.task
     1.6    type group = Task_Queue.group
     1.7 -  val thread_data: unit -> (string * task) option
     1.8 +  val is_worker: unit -> bool
     1.9    type 'a future
    1.10    val task_of: 'a future -> task
    1.11    val group_of: 'a future -> group
    1.12 @@ -40,6 +40,7 @@
    1.13    val fork_group: group -> (unit -> 'a) -> 'a future
    1.14    val fork_deps: 'b future list -> (unit -> 'a) -> 'a future
    1.15    val fork_pri: int -> (unit -> 'a) -> 'a future
    1.16 +  val fork_local: int -> (unit -> 'a) -> 'a future
    1.17    val join_results: 'a future list -> 'a Exn.result list
    1.18    val join_result: 'a future -> 'a Exn.result
    1.19    val join: 'a future -> 'a
    1.20 @@ -66,11 +67,16 @@
    1.21  type task = Task_Queue.task;
    1.22  type group = Task_Queue.group;
    1.23  
    1.24 -local val tag = Universal.tag () : (string * task) option Universal.tag in
    1.25 +local
    1.26 +  val tag = Universal.tag () : (string * task * group) option Universal.tag;
    1.27 +in
    1.28    fun thread_data () = the_default NONE (Thread.getLocal tag);
    1.29 -  fun setmp_thread_data data f x = Library.setmp_thread_data tag (thread_data ()) (SOME data) f x;
    1.30 +  fun setmp_thread_data data f x =
    1.31 +    Library.setmp_thread_data tag (thread_data ()) (SOME data) f x;
    1.32  end;
    1.33  
    1.34 +val is_worker = is_some o thread_data;
    1.35 +
    1.36  
    1.37  (* datatype future *)
    1.38  
    1.39 @@ -148,7 +154,7 @@
    1.40    let
    1.41      val _ = trace_active ();
    1.42      val valid = Task_Queue.is_valid group;
    1.43 -    val ok = setmp_thread_data (name, task) (fn () =>
    1.44 +    val ok = setmp_thread_data (name, task, group) (fn () =>
    1.45        fold (fn job => fn ok => job valid andalso ok) jobs true) ();
    1.46      val _ = SYNCHRONIZED "execute" (fn () =>
    1.47       (change queue (Task_Queue.finish task);
    1.48 @@ -277,6 +283,7 @@
    1.49  fun fork_group group e = fork_future (SOME group) [] 0 e;
    1.50  fun fork_deps deps e = fork_future NONE (map task_of deps) 0 e;
    1.51  fun fork_pri pri e = fork_future NONE [] pri e;
    1.52 +fun fork_local pri e = fork_future (Option.map #3 (thread_data ())) [] pri e;
    1.53  
    1.54  
    1.55  (* join *)
    1.56 @@ -300,13 +307,13 @@
    1.57        val _ = Multithreading.self_critical () andalso
    1.58          error "Cannot join future values within critical section";
    1.59  
    1.60 -      val is_worker = is_some (thread_data ());
    1.61 +      val worker = is_worker ();
    1.62        fun join_wait x =
    1.63          if SYNCHRONIZED "join_wait" (fn () =>
    1.64 -          is_finished x orelse (if is_worker then worker_wait () else wait (); false))
    1.65 +          is_finished x orelse (if worker then worker_wait () else wait (); false))
    1.66          then () else join_wait x;
    1.67  
    1.68 -      val _ = if is_worker then join_deps (map task_of xs) else ();
    1.69 +      val _ = if worker then join_deps (map task_of xs) else ();
    1.70        val _ = List.app join_wait xs;
    1.71  
    1.72      in map get_result xs end) ();
    1.73 @@ -342,7 +349,7 @@
    1.74  fun interruptible_task f x =
    1.75    if Multithreading.available then
    1.76      Multithreading.with_attributes
    1.77 -      (if is_some (thread_data ())
    1.78 +      (if is_worker ()
    1.79         then Multithreading.restricted_interrupts
    1.80         else Multithreading.regular_interrupts)
    1.81        (fn _ => f) x

     2.1 --- a/src/Pure/Isar/proof.ML	Sun Jul 19 17:08:34 2009 +0200
     2.2 +++ b/src/Pure/Isar/proof.ML	Sun Jul 19 18:02:40 2009 +0200
     2.3 @@ -1045,7 +1045,7 @@
     2.4  fun future_terminal_proof proof1 proof2 meths int state =
     2.5    if int orelse is_relevant state orelse not (Goal.future_enabled ())
     2.6    then proof1 meths state
     2.7 -  else snd (state |> proof2 (fn state' => Future.fork_pri ~1 (fn () => ((), proof1 meths state'))));
     2.8 +  else snd (proof2 (fn state' => Future.fork_local ~1 (fn () => ((), proof1 meths state'))) state);
     2.9  
    2.10  in
    2.11  

     3.1 --- a/src/Pure/Isar/toplevel.ML	Sun Jul 19 17:08:34 2009 +0200
     3.2 +++ b/src/Pure/Isar/toplevel.ML	Sun Jul 19 18:02:40 2009 +0200
     3.3 @@ -652,7 +652,7 @@
     3.4  
     3.5          val future_proof = Proof.global_future_proof
     3.6            (fn prf =>
     3.7 -            Future.fork_pri ~1 (fn () =>
     3.8 +            Future.fork_local ~1 (fn () =>
     3.9                let val (states, result_state) =
    3.10                  (case st' of State (SOME (Proof (_, (_, orig_gthy)), exit), prev)
    3.11                    => State (SOME (Proof (ProofNode.init prf, (finish, orig_gthy)), exit), prev))

     4.1 --- a/src/Pure/goal.ML	Sun Jul 19 17:08:34 2009 +0200
     4.2 +++ b/src/Pure/goal.ML	Sun Jul 19 18:02:40 2009 +0200
     4.3 @@ -98,7 +98,7 @@
     4.4  val parallel_proofs = ref true;
     4.5  
     4.6  fun future_enabled () =
     4.7 -  Future.enabled () andalso ! parallel_proofs andalso is_some (Future.thread_data ());
     4.8 +  Future.enabled () andalso ! parallel_proofs andalso Future.is_worker ();
     4.9  
    4.10  
    4.11  (* future_result *)
    4.12 @@ -185,7 +185,7 @@
    4.13      val res =
    4.14        if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse not (future_enabled ())
    4.15        then result ()
    4.16 -      else future_result ctxt' (Future.fork_pri ~1 result) (Thm.term_of stmt);
    4.17 +      else future_result ctxt' (Future.fork_local ~1 result) (Thm.term_of stmt);
    4.18    in
    4.19      Conjunction.elim_balanced (length props) res
    4.20      |> map (Assumption.export false ctxt' ctxt)