1.1 --- a/src/Pure/PIDE/command.ML	Thu Jul 11 16:35:37 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Thu Jul 11 18:41:05 2013 +0200
     1.3 @@ -54,10 +54,7 @@
     1.4                  let
     1.5                    val _ = Exec.running exec_id;
     1.6                    val res = Exn.capture (restore_attributes e) ();
     1.7 -                  val _ =
     1.8 -                    if Exn.is_interrupt_exn res
     1.9 -                    then Exec.canceled exec_id
    1.10 -                    else Exec.finished exec_id;
    1.11 +                  val _ = Exec.finished exec_id (not (Exn.is_interrupt_exn res));
    1.12                  in SOME (res, Result res) end) ())
    1.13        |> (fn NONE => error ("Concurrent execution attempt: " ^ Document_ID.print exec_id)
    1.14             | SOME res => res))

     2.1 --- a/src/Pure/PIDE/document.ML	Thu Jul 11 16:35:37 2013 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Thu Jul 11 18:41:05 2013 +0200
     2.3 @@ -314,7 +314,6 @@
     2.4    execution_of #> (fn {continue, ...} => Synchronized.change continue (K false));
     2.5  
     2.6  val cancel_execution = execution_of #> (fn {group, ...} => Future.cancel_group group);
     2.7 -val terminate_execution = execution_of #> (fn {group, ...} => Future.terminate group);
     2.8  
     2.9  fun start_execution state =
    2.10    let
    2.11 @@ -462,6 +461,11 @@
    2.12        val assign_update' = assign_update_new (command_id', SOME exec') assign_update;
    2.13        val init' = if Keyword.is_theory_begin command_name then NONE else init;
    2.14      in SOME (assign_update', (command_id', (eval', prints')), init') end;
    2.15 +
    2.16 +fun cancel_old_execs node0 (command_id, exec_ids) =
    2.17 +  subtract (op =) exec_ids (Command.exec_ids (lookup_entry node0 command_id))
    2.18 +  |> map_filter (Exec.peek_running #> Option.map (tap Future.cancel_group));
    2.19 +
    2.20  in
    2.21  
    2.22  fun update old_version_id new_version_id edits state =
    2.23 @@ -472,7 +476,6 @@
    2.24      val nodes = nodes_of new_version;
    2.25      val is_required = make_required nodes;
    2.26  
    2.27 -    val _ = timeit "Document.terminate_execution" (fn () => terminate_execution state);
    2.28      val updated = timeit "Document.update" (fn () =>
    2.29        nodes |> String_Graph.schedule
    2.30          (fn deps => fn (name, node) =>
    2.31 @@ -482,7 +485,7 @@
    2.32              (fn () =>
    2.33                let
    2.34                  val imports = map (apsnd Future.join) deps;
    2.35 -                val imports_changed = exists (#3 o #1 o #2) imports;
    2.36 +                val imports_changed = exists (#4 o #1 o #2) imports;
    2.37                  val node_required = is_required name;
    2.38                in
    2.39                  if imports_changed orelse AList.defined (op =) edits name orelse
    2.40 @@ -521,22 +524,29 @@
    2.41                        if is_none last_exec orelse is_some (after_entry node last_exec) then NONE
    2.42                        else SOME eval';
    2.43  
    2.44 +                    val assign_update = assign_update_result assigned_execs;
    2.45 +                    val old_groups = maps (cancel_old_execs node0) assign_update;
    2.46 +
    2.47                      val node' = node
    2.48                        |> assign_update_apply assigned_execs
    2.49                        |> entries_stable (assign_update_null updated_execs)
    2.50                        |> set_result result;
    2.51                      val assigned_node = SOME (name, node');
    2.52                      val result_changed = changed_result node0 node';
    2.53 -                  in
    2.54 -                    ((assign_update_result assigned_execs, assigned_node, result_changed), node')
    2.55 -                  end
    2.56 -                else (([], NONE, false), node)
    2.57 +                  in ((assign_update, old_groups, assigned_node, result_changed), node') end
    2.58 +                else (([], [], NONE, false), node)
    2.59                end))
    2.60        |> Future.joins |> map #1);
    2.61  
    2.62 +    val assign_update = maps #1 updated;
    2.63 +    val old_groups = maps #2 updated;
    2.64 +    val assigned_nodes = map_filter #3 updated;
    2.65 +
    2.66      val state' = state
    2.67 -      |> define_version new_version_id (fold put_node (map_filter #2 updated) new_version);
    2.68 -  in (maps #1 updated, state') end;
    2.69 +      |> define_version new_version_id (fold put_node assigned_nodes new_version);
    2.70 +
    2.71 +    val _ = timeit "Document.terminate" (fn () => List.app Future.terminate old_groups);
    2.72 +  in (assign_update, state') end;
    2.73  
    2.74  end;
    2.75  

     3.1 --- a/src/Pure/PIDE/exec.ML	Thu Jul 11 16:35:37 2013 +0200
     3.2 +++ b/src/Pure/PIDE/exec.ML	Thu Jul 11 18:41:05 2013 +0200
     3.3 @@ -6,39 +6,47 @@
     3.4  
     3.5  signature EXEC =
     3.6  sig
     3.7 +  val running: Document_ID.exec -> unit
     3.8 +  val finished: Document_ID.exec -> bool -> unit
     3.9    val is_stable: Document_ID.exec -> bool
    3.10 -  val running: Document_ID.exec -> unit
    3.11 -  val finished: Document_ID.exec -> unit
    3.12 -  val canceled: Document_ID.exec -> unit
    3.13 +  val peek_running: Document_ID.exec -> Future.group option
    3.14    val purge_unstable: unit -> unit
    3.15  end;
    3.16  
    3.17  structure Exec: EXEC =
    3.18  struct
    3.19  
    3.20 -val running_execs =
    3.21 -  Synchronized.var "Exec.running_execs" (Inttab.empty: {stable: bool} Inttab.table);
    3.22 +type status = Future.group option;  (*SOME group: running, NONE: canceled/unstable*)
    3.23 +val execs = Synchronized.var "Exec.execs" (Inttab.empty: status Inttab.table);
    3.24 +
    3.25 +fun running exec_id =
    3.26 +  let
    3.27 +    val group =
    3.28 +      (case Future.worker_group () of
    3.29 +        SOME group => group
    3.30 +      | NONE => error ("Missing worker thread context for execution " ^ Document_ID.print exec_id));
    3.31 +  in Synchronized.change execs (Inttab.update_new (exec_id, SOME group)) end;
    3.32 +
    3.33 +fun finished exec_id stable =
    3.34 +  Synchronized.change execs
    3.35 +    (if stable then Inttab.delete exec_id else Inttab.update (exec_id, NONE));
    3.36  
    3.37  fun is_stable exec_id =
    3.38    not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id))) andalso
    3.39 -  (case Inttab.lookup (Synchronized.value running_execs) exec_id of
    3.40 +  (case Inttab.lookup (Synchronized.value execs) exec_id of
    3.41      NONE => true
    3.42 -  | SOME {stable} => stable);
    3.43 +  | SOME status => is_some status);
    3.44  
    3.45 -fun running exec_id =
    3.46 -  Synchronized.change running_execs (Inttab.update_new (exec_id, {stable = true}));
    3.47 -
    3.48 -fun finished exec_id =
    3.49 -  Synchronized.change running_execs (Inttab.delete exec_id);
    3.50 -
    3.51 -fun canceled exec_id =
    3.52 -  Synchronized.change running_execs (Inttab.update (exec_id, {stable = false}));
    3.53 +fun peek_running exec_id =
    3.54 +  (case Inttab.lookup (Synchronized.value execs) exec_id of
    3.55 +    SOME (SOME group) => SOME group
    3.56 +  | _ => NONE);
    3.57  
    3.58  fun purge_unstable () =
    3.59 -  Synchronized.guarded_access running_execs
    3.60 +  Synchronized.guarded_access execs
    3.61      (fn tab =>
    3.62        let
    3.63 -        val unstable = Inttab.fold (fn (exec_id, {stable = false}) => cons exec_id | _ => I) tab [];
    3.64 +        val unstable = Inttab.fold (fn (exec_id, NONE) => cons exec_id | _ => I) tab [];
    3.65          val tab' = fold Inttab.delete unstable tab;
    3.66        in SOME ((), tab') end);
    3.67  

     4.1 --- a/src/Pure/PIDE/protocol.ML	Thu Jul 11 16:35:37 2013 +0200
     4.2 +++ b/src/Pure/PIDE/protocol.ML	Thu Jul 11 18:41:05 2013 +0200
     4.3 @@ -27,7 +27,7 @@
     4.4    Isabelle_Process.protocol_command "Document.update"
     4.5      (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
     4.6        let
     4.7 -        val _ = Document.cancel_execution state;
     4.8 +        val _ = Document.discontinue_execution state;
     4.9  
    4.10          val old_id = Document_ID.parse old_id_string;
    4.11          val new_id = Document_ID.parse new_id_string;