more careful termination of removed execs, leaving running execs undisturbed;

--- a/src/Pure/PIDE/document.ML	Sun Jul 14 00:08:15 2013 +0200
+++ b/src/Pure/PIDE/document.ML	Mon Jul 15 10:25:35 2013 +0200
@@ -21,7 +21,7 @@
   val start_execution: state -> unit
   val timing: bool Unsynchronized.ref
   val update: Document_ID.version -> Document_ID.version -> edit list -> state ->
-    (Document_ID.command * Document_ID.exec list) list * state
+    Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state
   val state: unit -> state
   val change_state: (state -> state) -> unit
 end;
@@ -444,9 +444,8 @@
       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 (Execution.peek #> Option.map (tap Future.cancel_group));
+fun removed_execs node0 (command_id, exec_ids) =
+  subtract (op =) exec_ids (Command.exec_ids (lookup_entry node0 command_id));
 
 in
 
@@ -507,7 +506,8 @@
                       else SOME eval';
 
                     val assign_update = assign_update_result assigned_execs;
-                    val old_groups = maps (cancel_old_execs node0) assign_update;
+                    val removed = maps (removed_execs node0) assign_update;
+                    val _ = List.app Execution.cancel removed;
 
                     val node' = node
                       |> assign_update_apply assigned_execs
@@ -515,20 +515,19 @@
                       |> set_result result;
                     val assigned_node = SOME (name, node');
                     val result_changed = changed_result node0 node';
-                  in ((assign_update, old_groups, assigned_node, result_changed), node') end
+                  in ((removed, assign_update, 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 removed = maps #1 updated;
+    val assign_update = maps #2 updated;
     val assigned_nodes = map_filter #3 updated;
 
     val state' = state
       |> 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;
+  in (removed, assign_update, state') end;
 
 end;
 

--- a/src/Pure/PIDE/execution.ML	Sun Jul 14 00:08:15 2013 +0200
+++ b/src/Pure/PIDE/execution.ML	Mon Jul 15 10:25:35 2013 +0200
@@ -12,7 +12,8 @@
   val is_running: Document_ID.execution -> bool
   val running: Document_ID.execution -> Document_ID.exec -> bool
   val finished: Document_ID.exec -> unit
-  val peek: Document_ID.exec -> Future.group option
+  val cancel: Document_ID.exec -> unit
+  val terminate: Document_ID.exec -> unit
   val snapshot: unit -> Future.group list
 end;
 
@@ -58,8 +59,11 @@
       Inttab.delete exec_id execs handle Inttab.UNDEF bad =>
         error ("Attempt to finish unknown execution " ^ Document_ID.print bad)));
 
-fun peek exec_id =
-  Inttab.lookup (snd (Synchronized.value state)) exec_id;
+fun peek_list exec_id =
+  the_list (Inttab.lookup (snd (Synchronized.value state)) exec_id);
+
+fun cancel exec_id = List.app Future.cancel_group (peek_list exec_id);
+fun terminate exec_id = List.app Future.terminate (peek_list exec_id);
 
 fun snapshot () =
   Inttab.fold (cons o #2) (snd (Synchronized.value state)) [];

--- a/src/Pure/PIDE/protocol.ML	Sun Jul 14 00:08:15 2013 +0200
+++ b/src/Pure/PIDE/protocol.ML	Mon Jul 15 10:25:35 2013 +0200
@@ -57,10 +57,9 @@
                   fn (a, []) => Document.Perspective (map int_atom a)]))
             end;
 
-        val (assign_update, state') = Document.update old_id new_id edits state;
-
-        val _ = List.app Future.cancel_group (Goal.reset_futures ());
-        val _ = Isabelle_Process.reset_tracing ();
+        val (removed, assign_update, state') = Document.update old_id new_id edits state;
+        val _ = List.app Execution.terminate removed;
+        val _ = List.app Isabelle_Process.reset_tracing removed;
 
         val _ =
           Output.protocol_message Markup.assign_update

--- a/src/Pure/System/isabelle_process.ML	Sun Jul 14 00:08:15 2013 +0200
+++ b/src/Pure/System/isabelle_process.ML	Mon Jul 15 10:25:35 2013 +0200
@@ -17,7 +17,7 @@
 sig
   val is_active: unit -> bool
   val protocol_command: string -> (string list -> unit) -> unit
-  val reset_tracing: unit -> unit
+  val reset_tracing: Document_ID.exec -> unit
   val crashes: exn list Synchronized.var
   val init_fifos: string -> string -> unit
   val init_socket: string -> unit
@@ -67,20 +67,20 @@
 val tracing_messages =
   Synchronized.var "tracing_messages" (Inttab.empty: int Inttab.table);
 
-fun reset_tracing () =
-  Synchronized.change tracing_messages (K Inttab.empty);
+fun reset_tracing exec_id =
+  Synchronized.change tracing_messages (Inttab.delete_safe exec_id);
 
 fun update_tracing () =
   (case Position.parse_id (Position.thread_data ()) of
     NONE => ()
-  | SOME id =>
+  | SOME exec_id =>
       let
         val ok =
           Synchronized.change_result tracing_messages (fn tab =>
             let
-              val n = the_default 0 (Inttab.lookup tab id) + 1;
+              val n = the_default 0 (Inttab.lookup tab exec_id) + 1;
               val ok = n <= Options.default_int "editor_tracing_messages";
-            in (ok, Inttab.update (id, n) tab) end);
+            in (ok, Inttab.update (exec_id, n) tab) end);
       in
         if ok then ()
         else
@@ -93,7 +93,7 @@
               handle Fail _ => error "Stopped";
           in
             Synchronized.change tracing_messages
-              (Inttab.map_default (id, 0) (fn k => k - m))
+              (Inttab.map_default (exec_id, 0) (fn k => k - m))
           end
       end);