tuned signature;
authorwenzelm
Tue Aug 23 17:43:06 2011 +0200 (2011-08-23)
changeset 44427c4a86d72a5cc
parent 44426 8d6869a8d4ec
child 44428 ccb8998f70b7
tuned signature;
src/Pure/Concurrent/future.ML
src/Pure/Concurrent/lazy.ML
     1.1 --- a/src/Pure/Concurrent/future.ML	Tue Aug 23 17:12:54 2011 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Tue Aug 23 17:43:06 2011 +0200
     1.3 @@ -54,10 +54,9 @@
     1.4    val interruptible_task: ('a -> 'b) -> 'a -> 'b
     1.5    val cancel_group: group -> task list
     1.6    val cancel: 'a future -> task list
     1.7 -  type fork_params =
     1.8 -    {name: string, group: group option, deps: task list, pri: int, interrupts: bool}
     1.9 -  val default_params: fork_params
    1.10 -  val forks: fork_params -> (unit -> 'a) list -> 'a future list
    1.11 +  type params = {name: string, group: group option, deps: task list, pri: int, interrupts: bool}
    1.12 +  val default_params: params
    1.13 +  val forks: params -> (unit -> 'a) list -> 'a future list
    1.14    val fork_pri: int -> (unit -> 'a) -> 'a future
    1.15    val fork: (unit -> 'a) -> 'a future
    1.16    val join_results: 'a future list -> 'a Exn.result list
    1.17 @@ -67,7 +66,7 @@
    1.18    val join_tasks: task list -> unit
    1.19    val value_result: 'a Exn.result -> 'a future
    1.20    val value: 'a -> 'a future
    1.21 -  val cond_forks: fork_params -> (unit -> 'a) list -> 'a future list
    1.22 +  val cond_forks: params -> (unit -> 'a) list -> 'a future list
    1.23    val map: ('a -> 'b) -> 'a future -> 'b future
    1.24    val promise_group: group -> (unit -> unit) -> 'a future
    1.25    val promise: (unit -> unit) -> 'a future
    1.26 @@ -459,13 +458,10 @@
    1.27  
    1.28  (* fork *)
    1.29  
    1.30 -type fork_params =
    1.31 -  {name: string, group: group option, deps: task list, pri: int, interrupts: bool};
    1.32 +type params = {name: string, group: group option, deps: task list, pri: int, interrupts: bool};
    1.33 +val default_params: params = {name = "", group = NONE, deps = [], pri = 0, interrupts = true};
    1.34  
    1.35 -val default_params: fork_params =
    1.36 -  {name = "", group = NONE, deps = [], pri = 0, interrupts = true};
    1.37 -
    1.38 -fun forks ({name, group, deps, pri, interrupts}: fork_params) es =
    1.39 +fun forks ({name, group, deps, pri, interrupts}: params) es =
    1.40    if null es then []
    1.41    else
    1.42      let
     2.1 --- a/src/Pure/Concurrent/lazy.ML	Tue Aug 23 17:12:54 2011 +0200
     2.2 +++ b/src/Pure/Concurrent/lazy.ML	Tue Aug 23 17:43:06 2011 +0200
     2.3 @@ -16,7 +16,7 @@
     2.4    val force_result: 'a lazy -> 'a Exn.result
     2.5    val force: 'a lazy -> 'a
     2.6    val map: ('a -> 'b) -> 'a lazy -> 'b lazy
     2.7 -  val future: Future.fork_params -> 'a lazy -> 'a future
     2.8 +  val future: Future.params -> 'a lazy -> 'a future
     2.9  end;
    2.10  
    2.11  structure Lazy: LAZY =