# HG changeset patch
# User wenzelm
# Date 1228430780 -3600
# Node ID 9d7ea903e8776ef646731f6229999a1994ad8121
# Parent  3ce619d8d4321aa98830b26e67e1efea393118a7
refined Future.fork interfaces, no longer export Future.future;

diff -r 3ce619d8d432 -r 9d7ea903e877 src/Pure/Concurrent/par_list.ML
--- a/src/Pure/Concurrent/par_list.ML	Thu Dec 04 23:46:20 2008 +0100
+++ b/src/Pure/Concurrent/par_list.ML	Thu Dec 04 23:46:20 2008 +0100
@@ -31,7 +31,7 @@
   if Future.enabled () then
     let
       val group = TaskQueue.new_group ();
-      val futures = map (fn x => Future.future (SOME group) [] true (fn () => f x)) xs;
+      val futures = map (fn x => Future.fork_group group (fn () => f x)) xs;
       val _ = List.app (ignore o Future.join_result) futures;
     in Future.join_results futures end
   else map (Exn.capture f) xs;
diff -r 3ce619d8d432 -r 9d7ea903e877 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Thu Dec 04 23:46:20 2008 +0100
+++ b/src/Pure/Thy/thy_info.ML	Thu Dec 04 23:46:20 2008 +0100
@@ -323,8 +323,8 @@
     fun future (name, body) tab =
       let
         val deps = map_filter (Symtab.lookup tab) (Graph.imm_preds task_graph name);
-        val x = Future.future NONE deps true body;
-      in (x, Symtab.update (name, Future.task_of x) tab) end;
+        val x = Future.fork_deps deps body;
+      in (x, Symtab.update (name, x) tab) end;
     val _ = ignore (Exn.release_all (Future.join_results (#1 (fold_map future tasks Symtab.empty))));
   in () end;