src/Pure/PIDE/document.ML

--- a/src/Pure/PIDE/document.ML	Thu Jul 11 16:35:37 2013 +0200
+++ b/src/Pure/PIDE/document.ML	Thu Jul 11 18:41:05 2013 +0200
@@ -314,7 +314,6 @@
   execution_of #> (fn {continue, ...} => Synchronized.change continue (K false));
 
 val cancel_execution = execution_of #> (fn {group, ...} => Future.cancel_group group);
-val terminate_execution = execution_of #> (fn {group, ...} => Future.terminate group);
 
 fun start_execution state =
   let
@@ -462,6 +461,11 @@
       val assign_update' = assign_update_new (command_id', SOME exec') assign_update;
       val init' = if Keyword.is_theory_begin command_name then NONE else init;
     in SOME (assign_update', (command_id', (eval', prints')), init') end;
+
+fun cancel_old_execs node0 (command_id, exec_ids) =
+  subtract (op =) exec_ids (Command.exec_ids (lookup_entry node0 command_id))
+  |> map_filter (Exec.peek_running #> Option.map (tap Future.cancel_group));
+
 in
 
 fun update old_version_id new_version_id edits state =
@@ -472,7 +476,6 @@
     val nodes = nodes_of new_version;
     val is_required = make_required nodes;
 
-    val _ = timeit "Document.terminate_execution" (fn () => terminate_execution state);
     val updated = timeit "Document.update" (fn () =>
       nodes |> String_Graph.schedule
         (fn deps => fn (name, node) =>
@@ -482,7 +485,7 @@
             (fn () =>
               let
                 val imports = map (apsnd Future.join) deps;
-                val imports_changed = exists (#3 o #1 o #2) imports;
+                val imports_changed = exists (#4 o #1 o #2) imports;
                 val node_required = is_required name;
               in
                 if imports_changed orelse AList.defined (op =) edits name orelse
@@ -521,22 +524,29 @@
                       if is_none last_exec orelse is_some (after_entry node last_exec) then NONE
                       else SOME eval';
 
+                    val assign_update = assign_update_result assigned_execs;
+                    val old_groups = maps (cancel_old_execs node0) assign_update;
+
                     val node' = node
                       |> assign_update_apply assigned_execs
                       |> entries_stable (assign_update_null updated_execs)
                       |> set_result result;
                     val assigned_node = SOME (name, node');
                     val result_changed = changed_result node0 node';
-                  in
-                    ((assign_update_result assigned_execs, assigned_node, result_changed), node')
-                  end
-                else (([], NONE, false), node)
+                  in ((assign_update, old_groups, assigned_node, result_changed), node') end
+                else (([], [], NONE, false), node)
               end))
       |> Future.joins |> map #1);
 
+    val assign_update = maps #1 updated;
+    val old_groups = maps #2 updated;
+    val assigned_nodes = map_filter #3 updated;
+
     val state' = state
-      |> define_version new_version_id (fold put_node (map_filter #2 updated) new_version);
-  in (maps #1 updated, state') end;
+      |> define_version new_version_id (fold put_node assigned_nodes new_version);
+
+    val _ = timeit "Document.terminate" (fn () => List.app Future.terminate old_groups);
+  in (assign_update, state') end;
 
 end;