tuned signature -- treat structure Task_Queue as private to implementation;

--- a/src/Pure/Concurrent/future.ML	Fri Aug 19 15:56:26 2011 +0200
+++ b/src/Pure/Concurrent/future.ML	Fri Aug 19 16:13:26 2011 +0200
@@ -41,17 +41,19 @@
 
 signature FUTURE =
 sig
-  val worker_task: unit -> Task_Queue.task option
-  val worker_group: unit -> Task_Queue.group option
-  val worker_subgroup: unit -> Task_Queue.group
+  type task = Task_Queue.task
+  type group = Task_Queue.group
+  val new_group: group option -> group
+  val worker_task: unit -> task option
+  val worker_group: unit -> group option
+  val worker_subgroup: unit -> group
   type 'a future
-  val task_of: 'a future -> Task_Queue.task
+  val task_of: 'a future -> task
   val peek: 'a future -> 'a Exn.result option
   val is_finished: 'a future -> bool
   val get_finished: 'a future -> 'a
   type fork_params =
-   {name: string, group: Task_Queue.group option, deps: Task_Queue.task list,
-    pri: int, interrupts: bool}
+    {name: string, group: group option, deps: task list, pri: int, interrupts: bool}
   val forks: fork_params -> (unit -> 'a) list -> 'a future list
   val fork_pri: int -> (unit -> 'a) -> 'a future
   val fork: (unit -> 'a) -> 'a future
@@ -61,11 +63,11 @@
   val value_result: 'a Exn.result -> 'a future
   val value: 'a -> 'a future
   val map: ('a -> 'b) -> 'a future -> 'b future
-  val cancel_group: Task_Queue.group -> unit future
+  val cancel_group: group -> unit future
   val cancel: 'a future -> unit future
   val interruptible_task: ('a -> 'b) -> 'a -> 'b
   val cond_forks: fork_params -> (unit -> 'a) list -> 'a future list
-  val promise_group: Task_Queue.group -> (unit -> unit) -> 'a future
+  val promise_group: group -> (unit -> unit) -> 'a future
   val promise: (unit -> unit) -> 'a future
   val fulfill_result: 'a future -> 'a Exn.result -> unit
   val fulfill: 'a future -> 'a -> unit
@@ -78,17 +80,22 @@
 
 (** future values **)
 
+type task = Task_Queue.task;
+type group = Task_Queue.group;
+val new_group = Task_Queue.new_group;
+
+
 (* identifiers *)
 
 local
-  val tag = Universal.tag () : Task_Queue.task option Universal.tag;
+  val tag = Universal.tag () : task option Universal.tag;
 in
   fun worker_task () = the_default NONE (Thread.getLocal tag);
   fun setmp_worker_task task f x = setmp_thread_data tag (worker_task ()) (SOME task) f x;
 end;
 
 val worker_group = Option.map Task_Queue.group_of_task o worker_task;
-fun worker_subgroup () = Task_Queue.new_group (worker_group ());
+fun worker_subgroup () = new_group (worker_group ());
 
 fun worker_joining e =
   (case worker_task () of
@@ -107,7 +114,7 @@
 
 datatype 'a future = Future of
  {promised: bool,
-  task: Task_Queue.task,
+  task: task,
   result: 'a result};
 
 fun task_of (Future {task, ...}) = task;
@@ -161,7 +168,7 @@
 val queue = Unsynchronized.ref Task_Queue.empty;
 val next = Unsynchronized.ref 0;
 val scheduler = Unsynchronized.ref (NONE: Thread.thread option);
-val canceled = Unsynchronized.ref ([]: Task_Queue.group list);
+val canceled = Unsynchronized.ref ([]: group list);
 val do_shutdown = Unsynchronized.ref false;
 val max_workers = Unsynchronized.ref 0;
 val max_active = Unsynchronized.ref 0;
@@ -432,8 +439,7 @@
 (* fork *)
 
 type fork_params =
- {name: string, group: Task_Queue.group option, deps: Task_Queue.task list,
-  pri: int, interrupts: bool};
+  {name: string, group: group option, deps: task list, pri: int, interrupts: bool};
 
 fun forks ({name, group, deps, pri, interrupts}: fork_params) es =
   if null es then []
@@ -529,7 +535,7 @@
 fun map_future f x =
   let
     val task = task_of x;
-    val group = Task_Queue.new_group (SOME (Task_Queue.group_of_task task));
+    val group = new_group (SOME (Task_Queue.group_of_task task));
     val (result, job) = future_job group true (fn () => f (join x));
 
     val extended = SYNCHRONIZED "extend" (fn () =>
@@ -557,7 +563,7 @@
     [] => value ()
   | running =>
       singleton
-        (forks {name = "cancel_group", group = SOME (Task_Queue.new_group NONE),
+        (forks {name = "cancel_group", group = SOME (new_group NONE),
           deps = running, pri = 0, interrupts = false}) I);
 
 fun cancel x = cancel_group (Task_Queue.group_of_task (task_of x));

--- a/src/Pure/Concurrent/par_list.ML	Fri Aug 19 15:56:26 2011 +0200
+++ b/src/Pure/Concurrent/par_list.ML	Fri Aug 19 16:13:26 2011 +0200
@@ -34,7 +34,7 @@
   then map (Exn.capture f) xs
   else
     let
-      val group = Task_Queue.new_group (Future.worker_group ());
+      val group = Future.new_group (Future.worker_group ());
       val futures =
         Future.forks {name = name, group = SOME group, deps = [], pri = 0, interrupts = true}
           (map (fn x => fn () => f x) xs);

--- a/src/Pure/PIDE/document.ML	Fri Aug 19 15:56:26 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Aug 19 16:13:26 2011 +0200
@@ -164,7 +164,7 @@
  {versions: version Inttab.table,  (*version_id -> document content*)
   commands: Toplevel.transition future Inttab.table,  (*command_id -> transition (future parsing)*)
   execs: Toplevel.state lazy Inttab.table,  (*exec_id -> execution process*)
-  execution: Task_Queue.group}  (*global execution process*)
+  execution: Future.group}  (*global execution process*)
 with
 
 fun make_state (versions, commands, execs, execution) =
@@ -177,7 +177,7 @@
   make_state (Inttab.make [(no_id, empty_version)],
     Inttab.make [(no_id, Future.value Toplevel.empty)],
     Inttab.make [(no_id, empty_exec)],
-    Task_Queue.new_group NONE);
+    Future.new_group NONE);
 
 
 (* document versions *)
@@ -254,7 +254,8 @@
   ignore
     (singleton
       (Future.forks {name = "Document.async_state",
-        group = SOME (Task_Queue.new_group NONE), deps = [], pri = 0, interrupts = true})
+        group = SOME (Future.new_group NONE),
+        deps = [], pri = 0, interrupts = true})
       (fn () =>
         Toplevel.setmp_thread_position tr
           (fn () => Toplevel.print_state false st) ()));
@@ -391,13 +392,13 @@
       fun force_exec NONE = ()
         | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
 
-      val execution = Task_Queue.new_group NONE;
+      val execution = Future.new_group NONE;
       val _ =
         nodes_of version |> Graph.schedule
           (fn deps => fn (name, node) =>
             singleton
               (Future.forks
-                {name = "theory:" ^ name, group = SOME (Task_Queue.new_group (SOME execution)),
+                {name = "theory:" ^ name, group = SOME (Future.new_group (SOME execution)),
                   deps = map (Future.task_of o #2) deps,
                   pri = 1, interrupts = true})
               (fold_entries NONE (fn (_, exec) => fn () => force_exec exec) node));