1.1 --- a/src/Pure/PIDE/command.ML	Fri Jul 12 11:28:03 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Fri Jul 12 12:04:16 2013 +0200
     1.3 @@ -8,8 +8,9 @@
     1.4  sig
     1.5    val read: (unit -> theory) -> Token.T list -> Toplevel.transition
     1.6    type eval
     1.7 +  val eval_eq: eval * eval -> bool
     1.8    val eval_result_state: eval -> Toplevel.state
     1.9 -  val eval_same: eval * eval -> bool
    1.10 +  val eval_stable: eval -> bool
    1.11    val eval: (unit -> theory) -> Token.T list -> eval -> eval
    1.12    type print
    1.13    val print: bool -> string -> eval -> print list -> print list option
    1.14 @@ -40,10 +41,15 @@
    1.15  
    1.16  fun memo_result (Memo v) =
    1.17    (case Synchronized.value v of
    1.18 -    Result res => Exn.release res
    1.19 -  | Expr (exec_id, _) => error ("Unfinished execution result: " ^ Document_ID.print exec_id));
    1.20 +    Expr (exec_id, _) => error ("Unfinished execution result: " ^ Document_ID.print exec_id)
    1.21 +  | Result res => Exn.release res);
    1.22  
    1.23 -fun memo_exec context (Memo v) =
    1.24 +fun memo_stable (Memo v) =
    1.25 +  (case Synchronized.value v of
    1.26 +   Expr _ => true
    1.27 + | Result res => not (Exn.is_interrupt_exn res));
    1.28 +
    1.29 +fun memo_exec execution_id (Memo v) =
    1.30    (case Synchronized.value v of
    1.31      Result res => res
    1.32    | Expr _ =>
    1.33 @@ -51,23 +57,24 @@
    1.34          (fn Result res => SOME (res, Result res)
    1.35            | expr as Expr (exec_id, e) =>
    1.36                uninterruptible (fn restore_attributes => fn () =>
    1.37 -                if Execution.running context exec_id then
    1.38 +                if Execution.running execution_id exec_id then
    1.39                    let
    1.40                      val res = Exn.capture (restore_attributes e) ();
    1.41 -                    val _ = Execution.finished exec_id (not (Exn.is_interrupt_exn res));
    1.42 +                    val _ = Execution.finished exec_id;
    1.43                    in SOME (res, Result res) end
    1.44                  else SOME (Exn.interrupt_exn, expr)) ())
    1.45        |> (fn NONE => error "Concurrent execution attempt" | SOME res => res))
    1.46    |> Exn.release |> ignore;
    1.47  
    1.48 -fun memo_fork params context (Memo v) =
    1.49 +fun memo_fork params execution_id (Memo v) =
    1.50    (case Synchronized.value v of
    1.51      Result _ => ()
    1.52 -  | _ => ignore ((singleton o Future.forks) params (fn () => memo_exec context (Memo v))));
    1.53 +  | _ => ignore ((singleton o Future.forks) params (fn () => memo_exec execution_id (Memo v))));
    1.54  
    1.55  end;
    1.56  
    1.57  
    1.58 +
    1.59  (** main phases of execution **)
    1.60  
    1.61  (* read *)
    1.62 @@ -109,11 +116,13 @@
    1.63  
    1.64  datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state memo};
    1.65  
    1.66 +fun eval_eq (Eval {exec_id, ...}, Eval {exec_id = exec_id', ...}) = exec_id = exec_id';
    1.67 +
    1.68  fun eval_result (Eval {eval_process, ...}) = memo_result eval_process;
    1.69  val eval_result_state = #state o eval_result;
    1.70  
    1.71 -fun eval_same (Eval {exec_id, ...}, Eval {exec_id = exec_id', ...}) =
    1.72 -  exec_id = exec_id' andalso Execution.is_stable exec_id;
    1.73 +fun eval_stable (Eval {exec_id, eval_process}) =
    1.74 +  Goal.stable_futures exec_id andalso memo_stable eval_process;
    1.75  
    1.76  local
    1.77  
    1.78 @@ -197,9 +206,12 @@
    1.79    (Toplevel.setmp_thread_position tr o Runtime.controlled_execution) e () handle exn =>
    1.80      List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
    1.81  
    1.82 +fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id';
    1.83 +
    1.84 +fun print_stable (Print {exec_id, print_process, ...}) =
    1.85 +  Goal.stable_futures exec_id andalso memo_stable print_process;
    1.86 +
    1.87  fun print_persistent (Print {persistent, ...}) = persistent;
    1.88 -fun print_stable (Print {exec_id, ...}) = Execution.is_stable exec_id;
    1.89 -fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id';
    1.90  
    1.91  in
    1.92  
    1.93 @@ -276,15 +288,15 @@
    1.94  
    1.95  local
    1.96  
    1.97 -fun run_print context (Print {name, pri, print_process, ...}) =
    1.98 +fun run_print execution_id (Print {name, pri, print_process, ...}) =
    1.99    (if Multithreading.enabled () then
   1.100      memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true}
   1.101 -  else memo_exec) context print_process;
   1.102 +  else memo_exec) execution_id print_process;
   1.103  
   1.104  in
   1.105  
   1.106 -fun exec context (Eval {eval_process, ...}, prints) =
   1.107 -  (memo_exec context eval_process; List.app (run_print context) prints);
   1.108 +fun exec execution_id (Eval {eval_process, ...}, prints) =
   1.109 +  (memo_exec execution_id eval_process; List.app (run_print execution_id) prints);
   1.110  
   1.111  end;
   1.112  

     2.1 --- a/src/Pure/PIDE/document.ML	Fri Jul 12 11:28:03 2013 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Fri Jul 12 12:04:16 2013 +0200
     2.3 @@ -108,7 +108,7 @@
     2.4  
     2.5  fun changed_result node node' =
     2.6    (case (get_result node, get_result node') of
     2.7 -    (SOME eval, SOME eval') => not (Command.eval_same (eval, eval'))
     2.8 +    (SOME eval, SOME eval') => not (Command.eval_eq (eval, eval'))
     2.9    | (NONE, NONE) => false
    2.10    | _ => true);
    2.11  
    2.12 @@ -401,7 +401,8 @@
    2.13            val flags' = update_flags prev flags;
    2.14            val same' =
    2.15              (case (lookup_entry node0 command_id, opt_exec) of
    2.16 -              (SOME (eval0, _), SOME (eval, _)) => Command.eval_same (eval0, eval)
    2.17 +              (SOME (eval0, _), SOME (eval, _)) =>
    2.18 +                Command.eval_eq (eval0, eval) andalso Command.eval_stable eval
    2.19              | _ => false);
    2.20            val assign_update' = assign_update |> same' ?
    2.21              (case opt_exec of
    2.22 @@ -445,7 +446,7 @@
    2.23  
    2.24  fun cancel_old_execs node0 (command_id, exec_ids) =
    2.25    subtract (op =) exec_ids (Command.exec_ids (lookup_entry node0 command_id))
    2.26 -  |> map_filter (Execution.peek_running #> Option.map (tap Future.cancel_group));
    2.27 +  |> map_filter (Execution.peek #> Option.map (tap Future.cancel_group));
    2.28  
    2.29  in
    2.30  

     3.1 --- a/src/Pure/PIDE/execution.ML	Fri Jul 12 11:28:03 2013 +0200
     3.2 +++ b/src/Pure/PIDE/execution.ML	Fri Jul 12 12:04:16 2013 +0200
     3.3 @@ -11,18 +11,17 @@
     3.4    val discontinue: unit -> unit
     3.5    val is_running: Document_ID.execution -> bool
     3.6    val running: Document_ID.execution -> Document_ID.exec -> bool
     3.7 -  val finished: Document_ID.exec -> bool -> unit
     3.8 -  val is_stable: Document_ID.exec -> bool
     3.9 -  val peek_running: Document_ID.exec -> Future.group option
    3.10 -  val purge_canceled: unit -> unit
    3.11 -  val terminate_all: unit -> unit
    3.12 +  val finished: Document_ID.exec -> unit
    3.13 +  val peek: Document_ID.exec -> Future.group option
    3.14 +  val snapshot: unit -> Future.group list
    3.15  end;
    3.16  
    3.17  structure Execution: EXECUTION =
    3.18  struct
    3.19  
    3.20 -type status = Future.group option;  (*SOME group: running, NONE: canceled*)
    3.21 -val state = Synchronized.var "Execution.state" (Document_ID.none, Inttab.empty: status Inttab.table);
    3.22 +val state =
    3.23 +  Synchronized.var "Execution.state"
    3.24 +    (Document_ID.none, Inttab.empty: Future.group Inttab.table);
    3.25  
    3.26  
    3.27  (* unique running execution *)
    3.28 @@ -48,46 +47,23 @@
    3.29          val continue = execution_id = execution_id';
    3.30          val execs' =
    3.31            if continue then
    3.32 -            Inttab.update_new (exec_id, SOME (Future.the_worker_group ())) execs
    3.33 +            Inttab.update_new (exec_id, Future.the_worker_group ()) execs
    3.34                handle Inttab.DUP dup => error ("Duplicate execution " ^ Document_ID.print dup)
    3.35            else execs;
    3.36        in SOME (continue, (execution_id', execs')) end);
    3.37  
    3.38 -fun finished exec_id stable =
    3.39 +fun finished exec_id =
    3.40    Synchronized.change state
    3.41      (apsnd (fn execs =>
    3.42 -      if not (Inttab.defined execs exec_id) then
    3.43 -        error ("Attempt to finish unknown execution: " ^ Document_ID.print exec_id)
    3.44 -      else if stable then Inttab.delete exec_id execs
    3.45 -      else Inttab.update (exec_id, NONE) execs));
    3.46 +      Inttab.delete exec_id execs
    3.47 +        handle Inttab.UNDEF bad =>
    3.48 +          error ("Attempt to finish unknown execution: " ^ Document_ID.print bad)));
    3.49  
    3.50 -fun is_stable exec_id =
    3.51 -  not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id))) andalso
    3.52 -  (case Inttab.lookup (snd (Synchronized.value state)) exec_id of
    3.53 -    NONE => true
    3.54 -  | SOME status => is_some status);
    3.55 +fun peek exec_id =
    3.56 +  Inttab.lookup (snd (Synchronized.value state)) exec_id;
    3.57  
    3.58 -fun peek_running exec_id =
    3.59 -  (case Inttab.lookup (snd (Synchronized.value state)) exec_id of
    3.60 -    SOME (SOME group) => SOME group
    3.61 -  | _ => NONE);
    3.62 -
    3.63 -fun purge_canceled () =
    3.64 -  Synchronized.guarded_access state
    3.65 -    (fn (execution_id, execs) =>
    3.66 -      let
    3.67 -        val canceled = Inttab.fold (fn (exec_id, NONE) => cons exec_id | _ => I) execs [];
    3.68 -        val execs' = fold Inttab.delete canceled execs;
    3.69 -      in SOME ((), (execution_id, execs')) end);
    3.70 -
    3.71 -fun terminate_all () =
    3.72 -  let
    3.73 -    val groups =
    3.74 -      Inttab.fold (fn (_, SOME group) => cons group | _ => I)
    3.75 -        (snd (Synchronized.value state)) [];
    3.76 -    val _ = List.app Future.cancel_group groups;
    3.77 -    val _ = List.app Future.terminate groups;
    3.78 -  in () end;
    3.79 +fun snapshot () =
    3.80 +  Inttab.fold (cons o #2) (snd (Synchronized.value state)) [];
    3.81  
    3.82  end;
    3.83  

     4.1 --- a/src/Pure/PIDE/protocol.ML	Fri Jul 12 11:28:03 2013 +0200
     4.2 +++ b/src/Pure/PIDE/protocol.ML	Fri Jul 12 12:04:16 2013 +0200
     4.3 @@ -21,7 +21,13 @@
     4.4  
     4.5  val _ =
     4.6    Isabelle_Process.protocol_command "Document.cancel_execution"
     4.7 -    (fn [] => (Execution.discontinue (); Execution.terminate_all ()));
     4.8 +    (fn [] =>
     4.9 +      let
    4.10 +        val _ = Execution.discontinue ();
    4.11 +        val groups = Execution.snapshot ();
    4.12 +        val _ = List.app Future.cancel_group groups;
    4.13 +        val _ = List.app Future.terminate groups;
    4.14 +      in () end);
    4.15  
    4.16  val _ =
    4.17    Isabelle_Process.protocol_command "Document.update"
    4.18 @@ -54,7 +60,6 @@
    4.19          val (assign_update, state') = Document.update old_id new_id edits state;
    4.20  
    4.21          val _ = List.app Future.cancel_group (Goal.reset_futures ());
    4.22 -        val _ = Execution.purge_canceled ();
    4.23          val _ = Isabelle_Process.reset_tracing ();
    4.24  
    4.25          val _ =

     5.1 --- a/src/Pure/goal.ML	Fri Jul 12 11:28:03 2013 +0200
     5.2 +++ b/src/Pure/goal.ML	Fri Jul 12 12:04:16 2013 +0200
     5.3 @@ -27,7 +27,8 @@
     5.4    val norm_result: thm -> thm
     5.5    val fork_params: {name: string, pos: Position.T, pri: int} -> (unit -> 'a) -> 'a future
     5.6    val fork: int -> (unit -> 'a) -> 'a future
     5.7 -  val peek_futures: serial -> unit future list
     5.8 +  val peek_futures: int -> unit future list
     5.9 +  val stable_futures: int-> bool
    5.10    val reset_futures: unit -> Future.group list
    5.11    val shutdown_futures: unit -> unit
    5.12    val skip_proofs_enabled: unit -> bool
    5.13 @@ -181,6 +182,9 @@
    5.14  fun peek_futures id =
    5.15    Inttab.lookup_list (#3 (Synchronized.value forked_proofs)) id;
    5.16  
    5.17 +fun stable_futures id =
    5.18 +  not (Par_Exn.is_interrupted (Future.join_results (peek_futures id)));
    5.19 +
    5.20  fun reset_futures () =
    5.21    Synchronized.change_result forked_proofs (fn (_, groups, _) =>
    5.22      (Future.forked_proofs := 0; (groups, (0, [], Inttab.empty))));