just one dedicated execution per document version -- NB: non-monotonicity of cancel always requires fresh update;
explicit terminate_execution;
tuned source structure;

--- a/src/Pure/PIDE/document.ML	Tue Apr 10 23:05:24 2012 +0200
+++ b/src/Pure/PIDE/document.ML	Wed Apr 11 11:44:21 2012 +0200
@@ -25,12 +25,12 @@
   type state
   val init_state: state
   val define_command: command_id -> string -> string -> state -> state
+  val remove_versions: version_id list -> state -> state
   val discontinue_execution: state -> unit
   val cancel_execution: state -> unit
-  val execute: version_id -> state -> state
+  val start_execution: state -> unit
   val update: version_id -> version_id -> edit list -> state ->
     (command_id * exec_id option) list * state
-  val remove_versions: version_id list -> state -> state
   val state: unit -> state
   val change_state: (state -> state) -> unit
 end;
@@ -144,7 +144,7 @@
     NONE => err_undef "command entry" id
   | SOME (exec, _) => exec);
 
-fun the_default_entry node (SOME id) = (id, (the_default (no_id, no_exec) (the_entry node id)))
+fun the_default_entry node (SOME id) = (id, the_default (no_id, no_exec) (the_entry node id))
   | the_default_entry _ NONE = (no_id, (no_id, no_exec));
 
 fun update_entry id exec =
@@ -220,14 +220,18 @@
   make_state (Inttab.make [(no_id, empty_version)], Inttab.empty,
     (no_id, Future.new_group NONE, Unsynchronized.ref false));
 
+fun execution_of (State {execution, ...}) = execution;
+
 
 (* document versions *)
 
 fun define_version (id: version_id) version =
-  map_state (fn (versions, commands, execution) =>
-    let val versions' = Inttab.update_new (id, version) versions
-      handle Inttab.DUP dup => err_dup "document version" dup
-    in (versions', commands, execution) end);
+  map_state (fn (versions, commands, _) =>
+    let
+      val versions' = Inttab.update_new (id, version) versions
+        handle Inttab.DUP dup => err_dup "document version" dup;
+      val execution' = (id, Future.new_group NONE, Unsynchronized.ref true);
+    in (versions', commands, execution') end);
 
 fun the_version (State {versions, ...}) (id: version_id) =
   (case Inttab.lookup versions id of
@@ -262,69 +266,72 @@
     NONE => err_undef "command" id
   | SOME command => command);
 
+end;
 
-(* document execution *)
-
-fun discontinue_execution (State {execution = (_, _, running), ...}) = running := false;
+fun remove_versions ids state = state |> map_state (fn (versions, _, execution) =>
+  let
+    val _ = member (op =) ids (#1 execution) andalso
+      error ("Attempt to remove execution version " ^ print_id (#1 execution));
 
-fun cancel_execution (State {execution = (_, group, _), ...}) = Future.cancel_group group;
-fun execution_tasks (State {execution = (_, group, _), ...}) = Future.group_tasks group;
-
-end;
+    val versions' = fold delete_version ids versions;
+    val commands' =
+      (versions', Inttab.empty) |->
+        Inttab.fold (fn (_, version) => nodes_of version |>
+          Graph.fold (fn (_, (node, _)) => node |>
+            iterate_entries (fn ((_, id), _) =>
+              SOME o Inttab.insert (K true) (id, the_command state id))));
+  in (versions', commands', execution) end);
 
 
 
-(** edit operations **)
+(** document execution **)
 
-(* execute *)
+val discontinue_execution = execution_of #> (fn (_, _, running) => running := false);
 
-local
+val cancel_execution = execution_of #> (fn (_, group, _) => Future.cancel_group group);
 
-fun finished_theory node =
-  (case Exn.capture (Command.memo_result o the) (get_result node) of
-    Exn.Res (st, _) => can (Toplevel.end_theory Position.none) st
-  | _ => false);
+fun terminate_execution state =
+  let
+    val (_, group, _) = execution_of state;
+    val _ = Future.cancel_group group;
+  in Future.join_tasks (Future.group_tasks group) end;
 
-in
-
-fun execute version_id state =
-  state |> map_state (fn (versions, commands, _) =>
-    let
-      val version = the_version state version_id;
+fun start_execution state =
+  let
+    fun finished_theory node =
+      (case Exn.capture (Command.memo_result o the) (get_result node) of
+        Exn.Res (st, _) => can (Toplevel.end_theory Position.none) st
+      | _ => false);
 
-      fun run node command_id exec =
-        let
-          val (_, print) = Command.memo_eval exec;
-          val _ =
-            if visible_command node command_id
-            then ignore (Lazy.future Future.default_params print)
-            else ();
-        in () end;
-
-      val group = Future.new_group NONE;
-      val running = Unsynchronized.ref true;
+    fun run node command_id exec =
+      let
+        val (_, print) = Command.memo_eval exec;
+        val _ =
+          if visible_command node command_id
+          then ignore (Lazy.future Future.default_params print)
+          else ();
+      in () end;
 
-      val _ =
-        nodes_of version |> Graph.schedule
-          (fn deps => fn (name, node) =>
-            if not (visible_node node) andalso finished_theory node then
-              Future.value ()
-            else
-              (singleton o Future.forks)
-                {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)),
-                  deps = map (Future.task_of o #2) deps, pri = ~2, interrupts = false}
-                (fn () =>
-                  iterate_entries (fn ((_, id), opt_exec) => fn () =>
-                    (case opt_exec of
-                      SOME (_, exec) => if ! running then SOME (run node id exec) else NONE
-                    | NONE => NONE)) node ()));
-
-    in (versions, commands, (version_id, group, running)) end);
-
-end;
+    val (version_id, group, running) = execution_of state;
+    val _ =
+      nodes_of (the_version state version_id) |> Graph.schedule
+        (fn deps => fn (name, node) =>
+          if not (visible_node node) andalso finished_theory node then
+            Future.value ()
+          else
+            (singleton o Future.forks)
+              {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)),
+                deps = map (Future.task_of o #2) deps, pri = ~2, interrupts = false}
+              (fn () =>
+                iterate_entries (fn ((_, id), opt_exec) => fn () =>
+                  (case opt_exec of
+                    SOME (_, exec) => if ! running then SOME (run node id exec) else NONE
+                  | NONE => NONE)) node ()));
+  in () end;
 
 
-(* update *)
+
+(** document update **)
 
 local
 
@@ -446,7 +453,7 @@
     val nodes = nodes_of new_version;
     val is_required = make_required nodes;
 
-    val _ = Future.join_tasks (execution_tasks state);
+    val _ = terminate_execution state;
     val updated =
       nodes |> Graph.schedule
         (fn deps => fn (name, node) =>
@@ -519,23 +526,6 @@
 end;
 
 
-(* remove versions *)
-
-fun remove_versions ids state = state |> map_state (fn (versions, _, execution) =>
-  let
-    val _ = member (op =) ids (#1 execution) andalso
-      error ("Attempt to remove execution version " ^ print_id (#1 execution));
-
-    val versions' = fold delete_version ids versions;
-    val commands' =
-      (versions', Inttab.empty) |->
-        Inttab.fold (fn (_, version) => nodes_of version |>
-          Graph.fold (fn (_, (node, _)) => node |>
-            iterate_entries (fn ((_, id), _) =>
-              SOME o Inttab.insert (K true) (id, the_command state id))));
-  in (versions', commands', execution) end);
-
-
 
 (** global state **)
 

--- a/src/Pure/PIDE/protocol.ML	Tue Apr 10 23:05:24 2012 +0200
+++ b/src/Pure/PIDE/protocol.ML	Wed Apr 11 11:44:21 2012 +0200
@@ -50,15 +50,16 @@
                   fn (a, []) => Document.Perspective (map int_atom a)]))
             end;
 
-        val (assignment, state1) = Document.update old_id new_id edits state;
+        val (assignment, state') = Document.update old_id new_id edits state;
         val _ =
           Output.protocol_message Isabelle_Markup.assign_execs
             ((new_id, assignment) |>
               let open XML.Encode
               in pair int (list (pair int (option int))) end
               |> YXML.string_of_body);
-        val state2 = Document.execute new_id state1;
-      in state2 end));
+
+        val _ = Document.start_execution state';
+      in state' end));
 
 val _ =
   Isabelle_Process.protocol_command "Document.remove_versions"