src/Pure/Concurrent/future.ML
changeset 28647 8068cdc84e7e
parent 28645 605a3b1ef6ba
child 28972 cb8a2c3e188f
equal deleted inserted replaced
28646:3a8d75c935ce 28647:8068cdc84e7e
    38   val is_finished: 'a T -> bool
    38   val is_finished: 'a T -> bool
    39   val future: group option -> task list -> bool -> (unit -> 'a) -> 'a T
    39   val future: group option -> task list -> bool -> (unit -> 'a) -> 'a T
    40   val fork: (unit -> 'a) -> 'a T
    40   val fork: (unit -> 'a) -> 'a T
    41   val fork_background: (unit -> 'a) -> 'a T
    41   val fork_background: (unit -> 'a) -> 'a T
    42   val join_results: 'a T list -> 'a Exn.result list
    42   val join_results: 'a T list -> 'a Exn.result list
       
    43   val join_result: 'a T -> 'a Exn.result
    43   val join: 'a T -> 'a
    44   val join: 'a T -> 'a
    44   val focus: task list -> unit
    45   val focus: task list -> unit
    45   val interrupt_task: string -> unit
    46   val interrupt_task: string -> unit
    46   val cancel: 'a T -> unit
    47   val cancel: 'a T -> unit
    47   val shutdown: unit -> unit
    48   val shutdown: unit -> unit
   256 fun join_results [] = []
   257 fun join_results [] = []
   257   | join_results xs = uninterruptible (fn _ => fn () =>
   258   | join_results xs = uninterruptible (fn _ => fn () =>
   258       let
   259       let
   259         val _ = scheduler_check "join check";
   260         val _ = scheduler_check "join check";
   260         val _ = Multithreading.self_critical () andalso
   261         val _ = Multithreading.self_critical () andalso
       
   262           exists (not o is_finished) xs andalso
   261           error "Cannot join future values within critical section";
   263           error "Cannot join future values within critical section";
   262 
   264 
   263         fun join_loop _ [] = ()
   265         fun join_loop _ [] = ()
   264           | join_loop name tasks =
   266           | join_loop name tasks =
   265               (case SYNCHRONIZED name (fn () =>
   267               (case SYNCHRONIZED name (fn () =>
   285                   do SYNCHRONIZED "join_task" (fn () => worker_wait "join_task");
   287                   do SYNCHRONIZED "join_task" (fn () => worker_wait "join_task");
   286               in () end);
   288               in () end);
   287 
   289 
   288       in xs |> map (fn Future {result = ref (SOME res), ...} => res) end) ();
   290       in xs |> map (fn Future {result = ref (SOME res), ...} => res) end) ();
   289 
   291 
   290 fun join x = Exn.release (singleton join_results x);
   292 fun join_result x = singleton join_results x;
       
   293 fun join x = Exn.release (join_result x);
   291 
   294 
   292 
   295 
   293 (* misc operations *)
   296 (* misc operations *)
   294 
   297 
   295 (*focus: collection of high-priority task*)
   298 (*focus: collection of high-priority task*)