src/Pure/PIDE/document.ML
changeset 44299 061599cb6eb0
parent 44271 89f40a5939b2
child 44300 349cc426d929
--- a/src/Pure/PIDE/document.ML	Fri Aug 19 14:01:20 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Aug 19 15:56:26 2011 +0200
@@ -24,7 +24,7 @@
   type state
   val init_state: state
   val join_commands: state -> unit
-  val cancel_execution: state -> unit -> unit
+  val cancel_execution: state -> unit future
   val define_command: command_id -> string -> state -> state
   val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
   val execute: version_id -> state -> state
@@ -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: unit future list}  (*global execution process*)
+  execution: Task_Queue.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);
 
 
 (* document versions *)
@@ -233,9 +233,7 @@
 
 (* document execution *)
 
-fun cancel_execution (State {execution, ...}) =
-  (List.app Future.cancel execution;
-    fn () => ignore (Future.join_results execution));
+fun cancel_execution (State {execution, ...}) = Future.cancel_group execution;
 
 end;
 
@@ -393,17 +391,18 @@
       fun force_exec NONE = ()
         | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
 
-      val execution' =
+      val execution = Task_Queue.new_group NONE;
+      val _ =
         nodes_of version |> Graph.schedule
           (fn deps => fn (name, node) =>
             singleton
               (Future.forks
-                {name = "theory:" ^ name, group = NONE,
+                {name = "theory:" ^ name, group = SOME (Task_Queue.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));
 
-    in (versions, commands, execs, execution') end);
+    in (versions, commands, execs, execution) end);