tuned signature -- treat structure Task_Queue as private to implementation;
authorwenzelm
Fri Aug 19 16:13:26 2011 +0200 (2011-08-19)
changeset 44300349cc426d929
parent 44299 061599cb6eb0
child 44301 65f60d9ac4bf
tuned signature -- treat structure Task_Queue as private to implementation;
src/Pure/Concurrent/future.ML
src/Pure/Concurrent/par_list.ML
src/Pure/PIDE/document.ML
     1.1 --- a/src/Pure/Concurrent/future.ML	Fri Aug 19 15:56:26 2011 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Fri Aug 19 16:13:26 2011 +0200
     1.3 @@ -41,17 +41,19 @@
     1.4  
     1.5  signature FUTURE =
     1.6  sig
     1.7 -  val worker_task: unit -> Task_Queue.task option
     1.8 -  val worker_group: unit -> Task_Queue.group option
     1.9 -  val worker_subgroup: unit -> Task_Queue.group
    1.10 +  type task = Task_Queue.task
    1.11 +  type group = Task_Queue.group
    1.12 +  val new_group: group option -> group
    1.13 +  val worker_task: unit -> task option
    1.14 +  val worker_group: unit -> group option
    1.15 +  val worker_subgroup: unit -> group
    1.16    type 'a future
    1.17 -  val task_of: 'a future -> Task_Queue.task
    1.18 +  val task_of: 'a future -> task
    1.19    val peek: 'a future -> 'a Exn.result option
    1.20    val is_finished: 'a future -> bool
    1.21    val get_finished: 'a future -> 'a
    1.22    type fork_params =
    1.23 -   {name: string, group: Task_Queue.group option, deps: Task_Queue.task list,
    1.24 -    pri: int, interrupts: bool}
    1.25 +    {name: string, group: group option, deps: task list, pri: int, interrupts: bool}
    1.26    val forks: fork_params -> (unit -> 'a) list -> 'a future list
    1.27    val fork_pri: int -> (unit -> 'a) -> 'a future
    1.28    val fork: (unit -> 'a) -> 'a future
    1.29 @@ -61,11 +63,11 @@
    1.30    val value_result: 'a Exn.result -> 'a future
    1.31    val value: 'a -> 'a future
    1.32    val map: ('a -> 'b) -> 'a future -> 'b future
    1.33 -  val cancel_group: Task_Queue.group -> unit future
    1.34 +  val cancel_group: group -> unit future
    1.35    val cancel: 'a future -> unit future
    1.36    val interruptible_task: ('a -> 'b) -> 'a -> 'b
    1.37    val cond_forks: fork_params -> (unit -> 'a) list -> 'a future list
    1.38 -  val promise_group: Task_Queue.group -> (unit -> unit) -> 'a future
    1.39 +  val promise_group: group -> (unit -> unit) -> 'a future
    1.40    val promise: (unit -> unit) -> 'a future
    1.41    val fulfill_result: 'a future -> 'a Exn.result -> unit
    1.42    val fulfill: 'a future -> 'a -> unit
    1.43 @@ -78,17 +80,22 @@
    1.44  
    1.45  (** future values **)
    1.46  
    1.47 +type task = Task_Queue.task;
    1.48 +type group = Task_Queue.group;
    1.49 +val new_group = Task_Queue.new_group;
    1.50 +
    1.51 +
    1.52  (* identifiers *)
    1.53  
    1.54  local
    1.55 -  val tag = Universal.tag () : Task_Queue.task option Universal.tag;
    1.56 +  val tag = Universal.tag () : task option Universal.tag;
    1.57  in
    1.58    fun worker_task () = the_default NONE (Thread.getLocal tag);
    1.59    fun setmp_worker_task task f x = setmp_thread_data tag (worker_task ()) (SOME task) f x;
    1.60  end;
    1.61  
    1.62  val worker_group = Option.map Task_Queue.group_of_task o worker_task;
    1.63 -fun worker_subgroup () = Task_Queue.new_group (worker_group ());
    1.64 +fun worker_subgroup () = new_group (worker_group ());
    1.65  
    1.66  fun worker_joining e =
    1.67    (case worker_task () of
    1.68 @@ -107,7 +114,7 @@
    1.69  
    1.70  datatype 'a future = Future of
    1.71   {promised: bool,
    1.72 -  task: Task_Queue.task,
    1.73 +  task: task,
    1.74    result: 'a result};
    1.75  
    1.76  fun task_of (Future {task, ...}) = task;
    1.77 @@ -161,7 +168,7 @@
    1.78  val queue = Unsynchronized.ref Task_Queue.empty;
    1.79  val next = Unsynchronized.ref 0;
    1.80  val scheduler = Unsynchronized.ref (NONE: Thread.thread option);
    1.81 -val canceled = Unsynchronized.ref ([]: Task_Queue.group list);
    1.82 +val canceled = Unsynchronized.ref ([]: group list);
    1.83  val do_shutdown = Unsynchronized.ref false;
    1.84  val max_workers = Unsynchronized.ref 0;
    1.85  val max_active = Unsynchronized.ref 0;
    1.86 @@ -432,8 +439,7 @@
    1.87  (* fork *)
    1.88  
    1.89  type fork_params =
    1.90 - {name: string, group: Task_Queue.group option, deps: Task_Queue.task list,
    1.91 -  pri: int, interrupts: bool};
    1.92 +  {name: string, group: group option, deps: task list, pri: int, interrupts: bool};
    1.93  
    1.94  fun forks ({name, group, deps, pri, interrupts}: fork_params) es =
    1.95    if null es then []
    1.96 @@ -529,7 +535,7 @@
    1.97  fun map_future f x =
    1.98    let
    1.99      val task = task_of x;
   1.100 -    val group = Task_Queue.new_group (SOME (Task_Queue.group_of_task task));
   1.101 +    val group = new_group (SOME (Task_Queue.group_of_task task));
   1.102      val (result, job) = future_job group true (fn () => f (join x));
   1.103  
   1.104      val extended = SYNCHRONIZED "extend" (fn () =>
   1.105 @@ -557,7 +563,7 @@
   1.106      [] => value ()
   1.107    | running =>
   1.108        singleton
   1.109 -        (forks {name = "cancel_group", group = SOME (Task_Queue.new_group NONE),
   1.110 +        (forks {name = "cancel_group", group = SOME (new_group NONE),
   1.111            deps = running, pri = 0, interrupts = false}) I);
   1.112  
   1.113  fun cancel x = cancel_group (Task_Queue.group_of_task (task_of x));
     2.1 --- a/src/Pure/Concurrent/par_list.ML	Fri Aug 19 15:56:26 2011 +0200
     2.2 +++ b/src/Pure/Concurrent/par_list.ML	Fri Aug 19 16:13:26 2011 +0200
     2.3 @@ -34,7 +34,7 @@
     2.4    then map (Exn.capture f) xs
     2.5    else
     2.6      let
     2.7 -      val group = Task_Queue.new_group (Future.worker_group ());
     2.8 +      val group = Future.new_group (Future.worker_group ());
     2.9        val futures =
    2.10          Future.forks {name = name, group = SOME group, deps = [], pri = 0, interrupts = true}
    2.11            (map (fn x => fn () => f x) xs);
     3.1 --- a/src/Pure/PIDE/document.ML	Fri Aug 19 15:56:26 2011 +0200
     3.2 +++ b/src/Pure/PIDE/document.ML	Fri Aug 19 16:13:26 2011 +0200
     3.3 @@ -164,7 +164,7 @@
     3.4   {versions: version Inttab.table,  (*version_id -> document content*)
     3.5    commands: Toplevel.transition future Inttab.table,  (*command_id -> transition (future parsing)*)
     3.6    execs: Toplevel.state lazy Inttab.table,  (*exec_id -> execution process*)
     3.7 -  execution: Task_Queue.group}  (*global execution process*)
     3.8 +  execution: Future.group}  (*global execution process*)
     3.9  with
    3.10  
    3.11  fun make_state (versions, commands, execs, execution) =
    3.12 @@ -177,7 +177,7 @@
    3.13    make_state (Inttab.make [(no_id, empty_version)],
    3.14      Inttab.make [(no_id, Future.value Toplevel.empty)],
    3.15      Inttab.make [(no_id, empty_exec)],
    3.16 -    Task_Queue.new_group NONE);
    3.17 +    Future.new_group NONE);
    3.18  
    3.19  
    3.20  (* document versions *)
    3.21 @@ -254,7 +254,8 @@
    3.22    ignore
    3.23      (singleton
    3.24        (Future.forks {name = "Document.async_state",
    3.25 -        group = SOME (Task_Queue.new_group NONE), deps = [], pri = 0, interrupts = true})
    3.26 +        group = SOME (Future.new_group NONE),
    3.27 +        deps = [], pri = 0, interrupts = true})
    3.28        (fn () =>
    3.29          Toplevel.setmp_thread_position tr
    3.30            (fn () => Toplevel.print_state false st) ()));
    3.31 @@ -391,13 +392,13 @@
    3.32        fun force_exec NONE = ()
    3.33          | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
    3.34  
    3.35 -      val execution = Task_Queue.new_group NONE;
    3.36 +      val execution = Future.new_group NONE;
    3.37        val _ =
    3.38          nodes_of version |> Graph.schedule
    3.39            (fn deps => fn (name, node) =>
    3.40              singleton
    3.41                (Future.forks
    3.42 -                {name = "theory:" ^ name, group = SOME (Task_Queue.new_group (SOME execution)),
    3.43 +                {name = "theory:" ^ name, group = SOME (Future.new_group (SOME execution)),
    3.44                    deps = map (Future.task_of o #2) deps,
    3.45                    pri = 1, interrupts = true})
    3.46                (fold_entries NONE (fn (_, exec) => fn () => force_exec exec) node));