src/Pure/PIDE/document.ML
changeset 52655 3b2b1ef13979
parent 52607 33a133d50616
child 52715 8979d830950b
     1.1 --- a/src/Pure/PIDE/document.ML	Sun Jul 14 00:08:15 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Mon Jul 15 10:25:35 2013 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4    val start_execution: state -> unit
     1.5    val timing: bool Unsynchronized.ref
     1.6    val update: Document_ID.version -> Document_ID.version -> edit list -> state ->
     1.7 -    (Document_ID.command * Document_ID.exec list) list * state
     1.8 +    Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state
     1.9    val state: unit -> state
    1.10    val change_state: (state -> state) -> unit
    1.11  end;
    1.12 @@ -444,9 +444,8 @@
    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 (Execution.peek #> Option.map (tap Future.cancel_group));
    1.19 +fun removed_execs node0 (command_id, exec_ids) =
    1.20 +  subtract (op =) exec_ids (Command.exec_ids (lookup_entry node0 command_id));
    1.21  
    1.22  in
    1.23  
    1.24 @@ -507,7 +506,8 @@
    1.25                        else SOME eval';
    1.26  
    1.27                      val assign_update = assign_update_result assigned_execs;
    1.28 -                    val old_groups = maps (cancel_old_execs node0) assign_update;
    1.29 +                    val removed = maps (removed_execs node0) assign_update;
    1.30 +                    val _ = List.app Execution.cancel removed;
    1.31  
    1.32                      val node' = node
    1.33                        |> assign_update_apply assigned_execs
    1.34 @@ -515,20 +515,19 @@
    1.35                        |> set_result result;
    1.36                      val assigned_node = SOME (name, node');
    1.37                      val result_changed = changed_result node0 node';
    1.38 -                  in ((assign_update, old_groups, assigned_node, result_changed), node') end
    1.39 +                  in ((removed, assign_update, assigned_node, result_changed), node') end
    1.40                  else (([], [], NONE, false), node)
    1.41                end))
    1.42        |> Future.joins |> map #1);
    1.43  
    1.44 -    val assign_update = maps #1 updated;
    1.45 -    val old_groups = maps #2 updated;
    1.46 +    val removed = maps #1 updated;
    1.47 +    val assign_update = maps #2 updated;
    1.48      val assigned_nodes = map_filter #3 updated;
    1.49  
    1.50      val state' = state
    1.51        |> define_version new_version_id (fold put_node assigned_nodes new_version);
    1.52  
    1.53 -    val _ = timeit "Document.terminate" (fn () => List.app Future.terminate old_groups);
    1.54 -  in (assign_update, state') end;
    1.55 +  in (removed, assign_update, state') end;
    1.56  
    1.57  end;
    1.58