--- a/src/Pure/Concurrent/future.ML Tue Aug 23 12:20:12 2011 +0200
+++ b/src/Pure/Concurrent/future.ML Tue Aug 23 15:48:41 2011 +0200
@@ -57,6 +57,7 @@
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
val fork_pri: int -> (unit -> 'a) -> 'a future
val fork: (unit -> 'a) -> 'a future
@@ -467,6 +468,9 @@
type fork_params =
{name: string, group: group option, deps: task list, pri: int, interrupts: bool};
+val default_params: fork_params =
+ {name = "", group = NONE, deps = [], pri = 0, interrupts = true};
+
fun forks ({name, group, deps, pri, interrupts}: fork_params) es =
if null es then []
else