src/Pure/Concurrent/future.ML
changeset 32107 47d0da617fcc
parent 32102 81d03a29980c
child 32109 ff3677972e3f
     1.1 --- a/src/Pure/Concurrent/future.ML	Tue Jul 21 20:37:32 2009 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Tue Jul 21 23:42:29 2009 +0200
     1.3 @@ -157,14 +157,19 @@
     1.4  fun future_job group (e: unit -> 'a) =
     1.5    let
     1.6      val result = ref (NONE: 'a Exn.result option);
     1.7 -    val job = Multithreading.with_attributes Multithreading.restricted_interrupts
     1.8 -      (fn _ => fn ok =>
     1.9 -        let
    1.10 -          val res = if ok then Exn.capture e () else Exn.Exn Exn.Interrupt;
    1.11 -          val _ = result := SOME res;
    1.12 -          val _ = (case res of Exn.Exn exn => Task_Queue.cancel_group group exn | _ => ());
    1.13 -          val res_ok = is_some (Exn.get_result res);
    1.14 -        in res_ok end);
    1.15 +    fun job ok =
    1.16 +      let
    1.17 +        val res =
    1.18 +          if ok then
    1.19 +            Multithreading.with_attributes Multithreading.restricted_interrupts
    1.20 +              (fn _ => fn () => Exn.capture e ()) ()
    1.21 +          else Exn.Exn Exn.Interrupt;
    1.22 +        val _ = result := SOME res;
    1.23 +      in
    1.24 +        (case res of
    1.25 +          Exn.Exn exn => (Task_Queue.cancel_group group exn; false)
    1.26 +        | Exn.Result _ => true)
    1.27 +      end;
    1.28    in (result, job) end;
    1.29  
    1.30  fun do_cancel group = (*requires SYNCHRONIZED*)
    1.31 @@ -203,7 +208,7 @@
    1.32      | some => some);
    1.33  
    1.34  fun worker_loop name =
    1.35 -  (case SYNCHRONIZED name worker_next of
    1.36 +  (case SYNCHRONIZED name (fn () => worker_next ()) of
    1.37      NONE => ()
    1.38    | SOME work => (execute name work; worker_loop name));
    1.39  
    1.40 @@ -259,7 +264,7 @@
    1.41    in continue end;
    1.42  
    1.43  fun scheduler_loop () =
    1.44 -  while SYNCHRONIZED "scheduler" scheduler_next do ();
    1.45 +  while SYNCHRONIZED "scheduler" (fn () => scheduler_next ()) do ();
    1.46  
    1.47  fun scheduler_active () = (*requires SYNCHRONIZED*)
    1.48    (case ! scheduler of NONE => false | SOME thread => Thread.isActive thread);