more careful termination of removed execs, leaving running execs undisturbed;
authorwenzelm
Mon Jul 15 10:25:35 2013 +0200 (2013-07-15)
changeset 526553b2b1ef13979
parent 52654 06653152ea8b
child 52656 9437f440ef3f
more careful termination of removed execs, leaving running execs undisturbed;
src/Pure/PIDE/document.ML
src/Pure/PIDE/execution.ML
src/Pure/PIDE/protocol.ML
src/Pure/System/isabelle_process.ML
     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  
     2.1 --- a/src/Pure/PIDE/execution.ML	Sun Jul 14 00:08:15 2013 +0200
     2.2 +++ b/src/Pure/PIDE/execution.ML	Mon Jul 15 10:25:35 2013 +0200
     2.3 @@ -12,7 +12,8 @@
     2.4    val is_running: Document_ID.execution -> bool
     2.5    val running: Document_ID.execution -> Document_ID.exec -> bool
     2.6    val finished: Document_ID.exec -> unit
     2.7 -  val peek: Document_ID.exec -> Future.group option
     2.8 +  val cancel: Document_ID.exec -> unit
     2.9 +  val terminate: Document_ID.exec -> unit
    2.10    val snapshot: unit -> Future.group list
    2.11  end;
    2.12  
    2.13 @@ -58,8 +59,11 @@
    2.14        Inttab.delete exec_id execs handle Inttab.UNDEF bad =>
    2.15          error ("Attempt to finish unknown execution " ^ Document_ID.print bad)));
    2.16  
    2.17 -fun peek exec_id =
    2.18 -  Inttab.lookup (snd (Synchronized.value state)) exec_id;
    2.19 +fun peek_list exec_id =
    2.20 +  the_list (Inttab.lookup (snd (Synchronized.value state)) exec_id);
    2.21 +
    2.22 +fun cancel exec_id = List.app Future.cancel_group (peek_list exec_id);
    2.23 +fun terminate exec_id = List.app Future.terminate (peek_list exec_id);
    2.24  
    2.25  fun snapshot () =
    2.26    Inttab.fold (cons o #2) (snd (Synchronized.value state)) [];
     3.1 --- a/src/Pure/PIDE/protocol.ML	Sun Jul 14 00:08:15 2013 +0200
     3.2 +++ b/src/Pure/PIDE/protocol.ML	Mon Jul 15 10:25:35 2013 +0200
     3.3 @@ -57,10 +57,9 @@
     3.4                    fn (a, []) => Document.Perspective (map int_atom a)]))
     3.5              end;
     3.6  
     3.7 -        val (assign_update, state') = Document.update old_id new_id edits state;
     3.8 -
     3.9 -        val _ = List.app Future.cancel_group (Goal.reset_futures ());
    3.10 -        val _ = Isabelle_Process.reset_tracing ();
    3.11 +        val (removed, assign_update, state') = Document.update old_id new_id edits state;
    3.12 +        val _ = List.app Execution.terminate removed;
    3.13 +        val _ = List.app Isabelle_Process.reset_tracing removed;
    3.14  
    3.15          val _ =
    3.16            Output.protocol_message Markup.assign_update
     4.1 --- a/src/Pure/System/isabelle_process.ML	Sun Jul 14 00:08:15 2013 +0200
     4.2 +++ b/src/Pure/System/isabelle_process.ML	Mon Jul 15 10:25:35 2013 +0200
     4.3 @@ -17,7 +17,7 @@
     4.4  sig
     4.5    val is_active: unit -> bool
     4.6    val protocol_command: string -> (string list -> unit) -> unit
     4.7 -  val reset_tracing: unit -> unit
     4.8 +  val reset_tracing: Document_ID.exec -> unit
     4.9    val crashes: exn list Synchronized.var
    4.10    val init_fifos: string -> string -> unit
    4.11    val init_socket: string -> unit
    4.12 @@ -67,20 +67,20 @@
    4.13  val tracing_messages =
    4.14    Synchronized.var "tracing_messages" (Inttab.empty: int Inttab.table);
    4.15  
    4.16 -fun reset_tracing () =
    4.17 -  Synchronized.change tracing_messages (K Inttab.empty);
    4.18 +fun reset_tracing exec_id =
    4.19 +  Synchronized.change tracing_messages (Inttab.delete_safe exec_id);
    4.20  
    4.21  fun update_tracing () =
    4.22    (case Position.parse_id (Position.thread_data ()) of
    4.23      NONE => ()
    4.24 -  | SOME id =>
    4.25 +  | SOME exec_id =>
    4.26        let
    4.27          val ok =
    4.28            Synchronized.change_result tracing_messages (fn tab =>
    4.29              let
    4.30 -              val n = the_default 0 (Inttab.lookup tab id) + 1;
    4.31 +              val n = the_default 0 (Inttab.lookup tab exec_id) + 1;
    4.32                val ok = n <= Options.default_int "editor_tracing_messages";
    4.33 -            in (ok, Inttab.update (id, n) tab) end);
    4.34 +            in (ok, Inttab.update (exec_id, n) tab) end);
    4.35        in
    4.36          if ok then ()
    4.37          else
    4.38 @@ -93,7 +93,7 @@
    4.39                handle Fail _ => error "Stopped";
    4.40            in
    4.41              Synchronized.change tracing_messages
    4.42 -              (Inttab.map_default (id, 0) (fn k => k - m))
    4.43 +              (Inttab.map_default (exec_id, 0) (fn k => k - m))
    4.44            end
    4.45        end);
    4.46