# HG changeset patch
# User wenzelm
# Date 1296511373 -3600
# Node ID 7da257539a8d4a3af787e0d2e3665c304d317d67
# Parent  1c191a39549f144f15c1d0a0f8422ac7c063d9f0
tuned signature;
tuned vacous forks;

diff -r 1c191a39549f -r 7da257539a8d src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Mon Jan 31 22:57:01 2011 +0100
+++ b/src/Pure/Concurrent/future.ML	Mon Jan 31 23:02:53 2011 +0100
@@ -44,7 +44,7 @@
   val group_of: 'a future -> group
   val peek: 'a future -> 'a Exn.result option
   val is_finished: 'a future -> bool
-  val bulk: {name: string, group: group option, deps: task list, pri: int} ->
+  val forks: {name: string, group: group option, deps: task list, pri: int} ->
     (unit -> 'a) list -> 'a future list
   val fork_pri: int -> (unit -> 'a) -> 'a future
   val fork: (unit -> 'a) -> 'a future
@@ -400,31 +400,33 @@
 
 (* fork *)
 
-fun bulk {name, group, deps, pri} es =
-  let
-    val grp =
-      (case group of
-        NONE => worker_subgroup ()
-      | SOME grp => grp);
-    fun enqueue e (minimal, queue) =
-      let
-        val (result, job) = future_job grp e;
-        val ((task, minimal'), queue') = Task_Queue.enqueue name grp deps pri job queue;
-        val future = Future {promised = false, task = task, group = grp, result = result};
-      in (future, (minimal orelse minimal', queue')) end;
-  in
-    SYNCHRONIZED "enqueue" (fn () =>
-      let
-        val (futures, minimal) =
-          Unsynchronized.change_result queue (fn q =>
-            let val (futures, (minimal, q')) = fold_map enqueue es (false, q)
-            in ((futures, minimal), q') end);
-        val _ = if minimal then signal work_available else ();
-        val _ = scheduler_check ();
-      in futures end)
-  end;
+fun forks {name, group, deps, pri} es =
+  if null es then []
+  else
+    let
+      val grp =
+        (case group of
+          NONE => worker_subgroup ()
+        | SOME grp => grp);
+      fun enqueue e (minimal, queue) =
+        let
+          val (result, job) = future_job grp e;
+          val ((task, minimal'), queue') = Task_Queue.enqueue name grp deps pri job queue;
+          val future = Future {promised = false, task = task, group = grp, result = result};
+        in (future, (minimal orelse minimal', queue')) end;
+    in
+      SYNCHRONIZED "enqueue" (fn () =>
+        let
+          val (futures, minimal) =
+            Unsynchronized.change_result queue (fn q =>
+              let val (futures, (minimal, q')) = fold_map enqueue es (false, q)
+              in ((futures, minimal), q') end);
+          val _ = if minimal then signal work_available else ();
+          val _ = scheduler_check ();
+        in futures end)
+    end;
 
-fun fork_pri pri e = singleton (bulk {name = "", group = NONE, deps = [], pri = pri}) e;
+fun fork_pri pri e = singleton (forks {name = "", group = NONE, deps = [], pri = pri}) e;
 fun fork e = fork_pri 0 e;
 
 
@@ -501,7 +503,7 @@
     if extended then Future {promised = false, task = task, group = group, result = result}
     else
       singleton
-        (bulk {name = "Future.map", group = SOME group,
+        (forks {name = "Future.map", group = SOME group,
           deps = [task], pri = Task_Queue.pri_of_task task})
         (fn () => f (join x))
   end;
diff -r 1c191a39549f -r 7da257539a8d src/Pure/Concurrent/par_list.ML
--- a/src/Pure/Concurrent/par_list.ML	Mon Jan 31 22:57:01 2011 +0100
+++ b/src/Pure/Concurrent/par_list.ML	Mon Jan 31 23:02:53 2011 +0100
@@ -31,7 +31,7 @@
     let
       val group = Task_Queue.new_group (Future.worker_group ());
       val futures =
-        Future.bulk {name = name, group = SOME group, deps = [], pri = 0}
+        Future.forks {name = name, group = SOME group, deps = [], pri = 0}
           (map (fn x => fn () => f x) xs);
       val results = Future.join_results futures
         handle exn => (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn);
diff -r 1c191a39549f -r 7da257539a8d src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Jan 31 22:57:01 2011 +0100
+++ b/src/Pure/Isar/toplevel.ML	Mon Jan 31 23:02:53 2011 +0100
@@ -664,7 +664,7 @@
         val future_proof = Proof.global_future_proof
           (fn prf =>
             singleton
-              (Future.bulk {name = "Toplevel.proof_result", group = NONE, deps = [], pri = ~1})
+              (Future.forks {name = "Toplevel.proof_result", group = NONE, deps = [], pri = ~1})
               (fn () =>
                 let val (states, result_state) =
                   (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
diff -r 1c191a39549f -r 7da257539a8d src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Mon Jan 31 22:57:01 2011 +0100
+++ b/src/Pure/PIDE/document.ML	Mon Jan 31 23:02:53 2011 +0100
@@ -209,7 +209,7 @@
 fun async_state tr st =
   ignore
     (singleton
-      (Future.bulk {name = "Document.async_state",
+      (Future.forks {name = "Document.async_state",
         group = SOME (Task_Queue.new_group NONE), deps = [], pri = 0})
       (fn () =>
         Toplevel.setmp_thread_position tr
@@ -339,7 +339,7 @@
       val _ = cancel state;
 
       val execution' = (* FIXME proper node deps *)
-        Future.bulk {name = "Document.execute", group = NONE, deps = [], pri = 1}
+        Future.forks {name = "Document.execute", group = NONE, deps = [], pri = 1}
           [fn () =>
             let
               val _ = await_cancellation state;
diff -r 1c191a39549f -r 7da257539a8d src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Mon Jan 31 22:57:01 2011 +0100
+++ b/src/Pure/Thy/thy_info.ML	Mon Jan 31 23:02:53 2011 +0100
@@ -187,7 +187,7 @@
 
             val future =
               singleton
-                (Future.bulk {name = "theory " ^ name, group = NONE, deps = task_deps, pri = 0})
+                (Future.forks {name = "theory " ^ name, group = NONE, deps = task_deps, pri = 0})
                 (fn () =>
                   (case map_filter failed deps of
                     [] => body (map (#1 o Future.join o get) parents)
diff -r 1c191a39549f -r 7da257539a8d src/Pure/goal.ML
--- a/src/Pure/goal.ML	Mon Jan 31 22:57:01 2011 +0100
+++ b/src/Pure/goal.ML	Mon Jan 31 23:02:53 2011 +0100
@@ -107,7 +107,7 @@
 (* parallel proofs *)
 
 fun fork e =
-  singleton (Future.bulk {name = "Goal.fork", group = NONE, deps = [], pri = ~1})
+  singleton (Future.forks {name = "Goal.fork", group = NONE, deps = [], pri = ~1})
     (fn () => Future.status e);
 
 val parallel_proofs = Unsynchronized.ref 1;
diff -r 1c191a39549f -r 7da257539a8d src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Mon Jan 31 22:57:01 2011 +0100
+++ b/src/Pure/proofterm.ML	Mon Jan 31 23:02:53 2011 +0100
@@ -1390,7 +1390,7 @@
       else Future.map postproc body
   | fulfill_proof_future thy promises postproc body =
       singleton
-        (Future.bulk {name = "Proofterm.fulfill_proof_future", group = NONE,
+        (Future.forks {name = "Proofterm.fulfill_proof_future", group = NONE,
             deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0})
         (fn () =>
           postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body)));
@@ -1448,7 +1448,7 @@
       else if not (Multithreading.enabled ()) then Future.value (make_body0 (full_proof0 ()))
       else
         singleton
-          (Future.bulk {name = "Proofterm.prepare_thm_proof", group = NONE, deps = [], pri = ~1})
+          (Future.forks {name = "Proofterm.prepare_thm_proof", group = NONE, deps = [], pri = ~1})
           (make_body0 o full_proof0);
 
     fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);