1.1 --- a/src/Pure/PIDE/document.ML	Fri Aug 19 14:01:20 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Aug 19 15:56:26 2011 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4    type state
     1.5    val init_state: state
     1.6    val join_commands: state -> unit
     1.7 -  val cancel_execution: state -> unit -> unit
     1.8 +  val cancel_execution: state -> unit future
     1.9    val define_command: command_id -> string -> state -> state
    1.10    val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
    1.11    val execute: version_id -> state -> state
    1.12 @@ -164,7 +164,7 @@
    1.13   {versions: version Inttab.table,  (*version_id -> document content*)
    1.14    commands: Toplevel.transition future Inttab.table,  (*command_id -> transition (future parsing)*)
    1.15    execs: Toplevel.state lazy Inttab.table,  (*exec_id -> execution process*)
    1.16 -  execution: unit future list}  (*global execution process*)
    1.17 +  execution: Task_Queue.group}  (*global execution process*)
    1.18  with
    1.19  
    1.20  fun make_state (versions, commands, execs, execution) =
    1.21 @@ -177,7 +177,7 @@
    1.22    make_state (Inttab.make [(no_id, empty_version)],
    1.23      Inttab.make [(no_id, Future.value Toplevel.empty)],
    1.24      Inttab.make [(no_id, empty_exec)],
    1.25 -    []);
    1.26 +    Task_Queue.new_group NONE);
    1.27  
    1.28  
    1.29  (* document versions *)
    1.30 @@ -233,9 +233,7 @@
    1.31  
    1.32  (* document execution *)
    1.33  
    1.34 -fun cancel_execution (State {execution, ...}) =
    1.35 -  (List.app Future.cancel execution;
    1.36 -    fn () => ignore (Future.join_results execution));
    1.37 +fun cancel_execution (State {execution, ...}) = Future.cancel_group execution;
    1.38  
    1.39  end;
    1.40  
    1.41 @@ -393,17 +391,18 @@
    1.42        fun force_exec NONE = ()
    1.43          | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
    1.44  
    1.45 -      val execution' =
    1.46 +      val execution = Task_Queue.new_group NONE;
    1.47 +      val _ =
    1.48          nodes_of version |> Graph.schedule
    1.49            (fn deps => fn (name, node) =>
    1.50              singleton
    1.51                (Future.forks
    1.52 -                {name = "theory:" ^ name, group = NONE,
    1.53 +                {name = "theory:" ^ name, group = SOME (Task_Queue.new_group (SOME execution)),
    1.54                    deps = map (Future.task_of o #2) deps,
    1.55                    pri = 1, interrupts = true})
    1.56                (fold_entries NONE (fn (_, exec) => fn () => force_exec exec) node));
    1.57  
    1.58 -    in (versions, commands, execs, execution') end);
    1.59 +    in (versions, commands, execs, execution) end);
    1.60  
    1.61  
    1.62