--- a/src/Pure/Concurrent/future.ML Tue Aug 23 17:12:54 2011 +0200
+++ b/src/Pure/Concurrent/future.ML Tue Aug 23 17:43:06 2011 +0200
@@ -54,10 +54,9 @@
val interruptible_task: ('a -> 'b) -> 'a -> 'b
val cancel_group: group -> task list
val cancel: 'a future -> task list
- type fork_params =
- {name: string, group: group option, deps: task list, pri: int, interrupts: bool}
- val default_params: fork_params
- val forks: fork_params -> (unit -> 'a) list -> 'a future list
+ type params = {name: string, group: group option, deps: task list, pri: int, interrupts: bool}
+ val default_params: params
+ val forks: params -> (unit -> 'a) list -> 'a future list
val fork_pri: int -> (unit -> 'a) -> 'a future
val fork: (unit -> 'a) -> 'a future
val join_results: 'a future list -> 'a Exn.result list
@@ -67,7 +66,7 @@
val join_tasks: task list -> unit
val value_result: 'a Exn.result -> 'a future
val value: 'a -> 'a future
- val cond_forks: fork_params -> (unit -> 'a) list -> 'a future list
+ val cond_forks: params -> (unit -> 'a) list -> 'a future list
val map: ('a -> 'b) -> 'a future -> 'b future
val promise_group: group -> (unit -> unit) -> 'a future
val promise: (unit -> unit) -> 'a future
@@ -459,13 +458,10 @@
(* fork *)
-type fork_params =
- {name: string, group: group option, deps: task list, pri: int, interrupts: bool};
+type params = {name: string, group: group option, deps: task list, pri: int, interrupts: bool};
+val default_params: params = {name = "", group = NONE, deps = [], pri = 0, interrupts = true};
-val default_params: fork_params =
- {name = "", group = NONE, deps = [], pri = 0, interrupts = true};
-
-fun forks ({name, group, deps, pri, interrupts}: fork_params) es =
+fun forks ({name, group, deps, pri, interrupts}: params) es =
if null es then []
else
let
--- a/src/Pure/Concurrent/lazy.ML Tue Aug 23 17:12:54 2011 +0200
+++ b/src/Pure/Concurrent/lazy.ML Tue Aug 23 17:43:06 2011 +0200
@@ -16,7 +16,7 @@
val force_result: 'a lazy -> 'a Exn.result
val force: 'a lazy -> 'a
val map: ('a -> 'b) -> 'a lazy -> 'b lazy
- val future: Future.fork_params -> 'a lazy -> 'a future
+ val future: Future.params -> 'a lazy -> 'a future
end;
structure Lazy: LAZY =