src/Pure/PIDE/document.ML
changeset 52602 00170ef1dc39
parent 52600 75afb82daf5c
child 52604 ff2f0818aebc
     1.1 --- a/src/Pure/PIDE/document.ML	Thu Jul 11 16:35:37 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Thu Jul 11 18:41:05 2013 +0200
     1.3 @@ -314,7 +314,6 @@
     1.4    execution_of #> (fn {continue, ...} => Synchronized.change continue (K false));
     1.5  
     1.6  val cancel_execution = execution_of #> (fn {group, ...} => Future.cancel_group group);
     1.7 -val terminate_execution = execution_of #> (fn {group, ...} => Future.terminate group);
     1.8  
     1.9  fun start_execution state =
    1.10    let
    1.11 @@ -462,6 +461,11 @@
    1.12        val assign_update' = assign_update_new (command_id', SOME exec') assign_update;
    1.13        val init' = if Keyword.is_theory_begin command_name then NONE else init;
    1.14      in SOME (assign_update', (command_id', (eval', prints')), init') end;
    1.15 +
    1.16 +fun cancel_old_execs node0 (command_id, exec_ids) =
    1.17 +  subtract (op =) exec_ids (Command.exec_ids (lookup_entry node0 command_id))
    1.18 +  |> map_filter (Exec.peek_running #> Option.map (tap Future.cancel_group));
    1.19 +
    1.20  in
    1.21  
    1.22  fun update old_version_id new_version_id edits state =
    1.23 @@ -472,7 +476,6 @@
    1.24      val nodes = nodes_of new_version;
    1.25      val is_required = make_required nodes;
    1.26  
    1.27 -    val _ = timeit "Document.terminate_execution" (fn () => terminate_execution state);
    1.28      val updated = timeit "Document.update" (fn () =>
    1.29        nodes |> String_Graph.schedule
    1.30          (fn deps => fn (name, node) =>
    1.31 @@ -482,7 +485,7 @@
    1.32              (fn () =>
    1.33                let
    1.34                  val imports = map (apsnd Future.join) deps;
    1.35 -                val imports_changed = exists (#3 o #1 o #2) imports;
    1.36 +                val imports_changed = exists (#4 o #1 o #2) imports;
    1.37                  val node_required = is_required name;
    1.38                in
    1.39                  if imports_changed orelse AList.defined (op =) edits name orelse
    1.40 @@ -521,22 +524,29 @@
    1.41                        if is_none last_exec orelse is_some (after_entry node last_exec) then NONE
    1.42                        else SOME eval';
    1.43  
    1.44 +                    val assign_update = assign_update_result assigned_execs;
    1.45 +                    val old_groups = maps (cancel_old_execs node0) assign_update;
    1.46 +
    1.47                      val node' = node
    1.48                        |> assign_update_apply assigned_execs
    1.49                        |> entries_stable (assign_update_null updated_execs)
    1.50                        |> set_result result;
    1.51                      val assigned_node = SOME (name, node');
    1.52                      val result_changed = changed_result node0 node';
    1.53 -                  in
    1.54 -                    ((assign_update_result assigned_execs, assigned_node, result_changed), node')
    1.55 -                  end
    1.56 -                else (([], NONE, false), node)
    1.57 +                  in ((assign_update, old_groups, assigned_node, result_changed), node') end
    1.58 +                else (([], [], NONE, false), node)
    1.59                end))
    1.60        |> Future.joins |> map #1);
    1.61  
    1.62 +    val assign_update = maps #1 updated;
    1.63 +    val old_groups = maps #2 updated;
    1.64 +    val assigned_nodes = map_filter #3 updated;
    1.65 +
    1.66      val state' = state
    1.67 -      |> define_version new_version_id (fold put_node (map_filter #2 updated) new_version);
    1.68 -  in (maps #1 updated, state') end;
    1.69 +      |> define_version new_version_id (fold put_node assigned_nodes new_version);
    1.70 +
    1.71 +    val _ = timeit "Document.terminate" (fn () => List.app Future.terminate old_groups);
    1.72 +  in (assign_update, state') end;
    1.73  
    1.74  end;
    1.75