1.1 --- a/src/Pure/PIDE/command.ML	Thu Jul 11 12:28:24 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Thu Jul 11 14:42:11 2013 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4    type eval_process
     1.5    type eval = {exec_id: Document_ID.exec, eval_process: eval_process}
     1.6    val eval_result_state: eval -> Toplevel.state
     1.7 +  val eval_same: eval * eval -> bool
     1.8    type print_process
     1.9    type print =
    1.10     {name: string, pri: int, persistent: bool,
    1.11 @@ -16,9 +17,6 @@
    1.12    type exec = eval * print list
    1.13    val no_exec: exec
    1.14    val exec_ids: exec option -> Document_ID.exec list
    1.15 -  val stable_eval: eval -> bool
    1.16 -  val stable_print: print -> bool
    1.17 -  val same_eval: eval * eval -> bool
    1.18    val read: (unit -> theory) -> Token.T list -> Toplevel.transition
    1.19    val eval: (unit -> theory) -> Token.T list -> eval -> eval
    1.20    val print: bool -> string -> eval -> print list -> print list option
    1.21 @@ -35,40 +33,42 @@
    1.22  (** memo results -- including physical interrupts! **)
    1.23  
    1.24  datatype 'a expr =
    1.25 -  Expr of unit -> 'a |
    1.26 +  Expr of Document_ID.exec * (unit -> 'a) |
    1.27    Result of 'a Exn.result;
    1.28  
    1.29  abstype 'a memo = Memo of 'a expr Synchronized.var
    1.30  with
    1.31  
    1.32 -fun memo e = Memo (Synchronized.var "Command.memo" (Expr e));
    1.33 +fun memo exec_id e = Memo (Synchronized.var "Command.memo" (Expr (exec_id, e)));
    1.34  fun memo_value a = Memo (Synchronized.var "Command.memo" (Result (Exn.Res a)));
    1.35  
    1.36 -fun memo_eval (Memo v) =
    1.37 -  (case Synchronized.value v of
    1.38 -    Result res => res
    1.39 -  | _ =>
    1.40 -      Synchronized.guarded_access v
    1.41 -        (fn Result res => SOME (res, Result res)
    1.42 -          | Expr e =>
    1.43 -              let val res = Exn.capture e ();  (*sic!*)
    1.44 -              in SOME (res, Result res) end))
    1.45 -  |> Exn.release;
    1.46 -
    1.47 -fun memo_fork params (Memo v) =
    1.48 -  (case Synchronized.value v of
    1.49 -    Result _ => ()
    1.50 -  | _ => ignore ((singleton o Future.forks) params (fn () => memo_eval (Memo v))));
    1.51 -
    1.52  fun memo_result (Memo v) =
    1.53    (case Synchronized.value v of
    1.54      Result res => Exn.release res
    1.55    | _ => raise Fail "Unfinished memo result");
    1.56  
    1.57 -fun memo_stable (Memo v) =
    1.58 +fun memo_exec (Memo v) =
    1.59    (case Synchronized.value v of
    1.60 -    Expr _ => true
    1.61 -  | Result res => not (Exn.is_interrupt_exn res));
    1.62 +    Result res => res
    1.63 +  | _ =>
    1.64 +      Synchronized.guarded_access v
    1.65 +        (fn Result res => SOME (res, Result res)
    1.66 +          | Expr (exec_id, e) =>
    1.67 +              uninterruptible (fn restore_attributes => fn () =>
    1.68 +                let
    1.69 +                  val _ = Exec.running exec_id;
    1.70 +                  val res = Exn.capture (restore_attributes e) ();
    1.71 +                  val _ =
    1.72 +                    if Exn.is_interrupt_exn res
    1.73 +                    then Exec.canceled exec_id
    1.74 +                    else Exec.finished exec_id;
    1.75 +                in SOME (res, Result res) end) ()))
    1.76 +  |> Exn.release;
    1.77 +
    1.78 +fun memo_fork params (Memo v) =
    1.79 +  (case Synchronized.value v of
    1.80 +    Result _ => ()
    1.81 +  | _ => ignore ((singleton o Future.forks) params (fn () => memo_exec (Memo v))));
    1.82  
    1.83  end;
    1.84  
    1.85 @@ -76,7 +76,7 @@
    1.86  
    1.87  (** main phases of execution **)
    1.88  
    1.89 -(* basic type definitions *)
    1.90 +(* type definitions *)
    1.91  
    1.92  type eval_state =
    1.93    {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state};
    1.94 @@ -89,6 +89,9 @@
    1.95  fun eval_result ({eval_process, ...}: eval) = memo_result eval_process;
    1.96  val eval_result_state = #state o eval_result;
    1.97  
    1.98 +fun eval_same ({exec_id, ...}: eval, {exec_id = exec_id', ...}: eval) =
    1.99 +  exec_id = exec_id' andalso Exec.is_stable exec_id;
   1.100 +
   1.101  type print_process = unit memo;
   1.102  type print =
   1.103   {name: string, pri: int, persistent: bool,
   1.104 @@ -101,21 +104,6 @@
   1.105    | exec_ids (SOME ({exec_id, ...}, prints)) = exec_id :: map #exec_id prints;
   1.106  
   1.107  
   1.108 -(* stable results *)
   1.109 -
   1.110 -fun stable_goals exec_id =
   1.111 -  not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id)));
   1.112 -
   1.113 -fun stable_eval ({exec_id, eval_process}: eval) =
   1.114 -  stable_goals exec_id andalso memo_stable eval_process;
   1.115 -
   1.116 -fun stable_print ({exec_id, print_process, ...}: print) =
   1.117 -  stable_goals exec_id andalso memo_stable print_process;
   1.118 -
   1.119 -fun same_eval (eval: eval, eval': eval) =
   1.120 -  #exec_id eval = #exec_id eval' andalso stable_eval eval';
   1.121 -
   1.122 -
   1.123  (* read *)
   1.124  
   1.125  fun read init span =
   1.126 @@ -208,7 +196,7 @@
   1.127            Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id))
   1.128              (fn () => read init span |> Toplevel.exec_id exec_id) ();
   1.129        in eval_state span tr (eval_result eval0) end;
   1.130 -  in {exec_id = exec_id, eval_process = memo process} end;
   1.131 +  in {exec_id = exec_id, eval_process = memo exec_id process} end;
   1.132  
   1.133  end;
   1.134  
   1.135 @@ -226,6 +214,8 @@
   1.136    (Toplevel.setmp_thread_position tr o Runtime.controlled_execution) e () handle exn =>
   1.137      List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
   1.138  
   1.139 +fun print_stable (print: print) = Exec.is_stable (#exec_id print);
   1.140 +
   1.141  in
   1.142  
   1.143  fun print command_visible command_name eval old_prints =
   1.144 @@ -245,7 +235,7 @@
   1.145                end;
   1.146            in
   1.147             {name = name, pri = pri, persistent = persistent,
   1.148 -            exec_id = exec_id, print_process = memo process}
   1.149 +            exec_id = exec_id, print_process = memo exec_id process}
   1.150            end;
   1.151        in
   1.152          (case Exn.capture (Runtime.controlled_execution get_fn) {command_name = command_name} of
   1.153 @@ -258,9 +248,9 @@
   1.154        if command_visible then
   1.155          rev (Synchronized.value print_functions) |> map_filter (fn pr =>
   1.156            (case find_first (equal (fst pr) o #name) old_prints of
   1.157 -            SOME print => if stable_print print then SOME print else new_print pr
   1.158 +            SOME print => if print_stable print then SOME print else new_print pr
   1.159            | NONE => new_print pr))
   1.160 -      else filter (fn print => #persistent print andalso stable_print print) old_prints;
   1.161 +      else filter (fn print => #persistent print andalso print_stable print) old_prints;
   1.162    in
   1.163      if eq_list (op = o pairself #exec_id) (old_prints, new_prints) then NONE
   1.164      else SOME new_prints
   1.165 @@ -289,15 +279,15 @@
   1.166        in if do_print then Toplevel.print_state false st' else () end));
   1.167  
   1.168  
   1.169 -(* overall execution process *)
   1.170 +(* combined execution process *)
   1.171  
   1.172  fun run_print ({name, pri, print_process, ...}: print) =
   1.173    (if Multithreading.enabled () then
   1.174      memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true}
   1.175 -  else memo_eval) print_process;
   1.176 +  else memo_exec) print_process;
   1.177  
   1.178  fun execute (({eval_process, ...}, prints): exec) =
   1.179 -  (memo_eval eval_process; List.app run_print prints);
   1.180 +  (memo_exec eval_process; List.app run_print prints);
   1.181  
   1.182  end;
   1.183  

     2.1 --- a/src/Pure/PIDE/document.ML	Thu Jul 11 12:28:24 2013 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Thu Jul 11 14:42:11 2013 +0200
     2.3 @@ -421,7 +421,7 @@
     2.4            val flags' = update_flags prev flags;
     2.5            val same' =
     2.6              (case (lookup_entry node0 command_id, opt_exec) of
     2.7 -              (SOME (eval0, _), SOME (eval, _)) => Command.same_eval (eval0, eval)
     2.8 +              (SOME (eval0, _), SOME (eval, _)) => Command.eval_same (eval0, eval)
     2.9              | _ => false);
    2.10            val assign_update' = assign_update |> same' ?
    2.11              (case opt_exec of

     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/PIDE/exec.ML	Thu Jul 11 14:42:11 2013 +0200
     3.3 @@ -0,0 +1,46 @@
     3.4 +(*  Title:      Pure/PIDE/exec.ML
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Global management of command execution fragments.
     3.8 +*)
     3.9 +
    3.10 +signature EXEC =
    3.11 +sig
    3.12 +  val is_stable: Document_ID.exec -> bool
    3.13 +  val running: Document_ID.exec -> unit
    3.14 +  val finished: Document_ID.exec -> unit
    3.15 +  val canceled: Document_ID.exec -> unit
    3.16 +  val purge_unstable: unit -> unit
    3.17 +end;
    3.18 +
    3.19 +structure Exec: EXEC =
    3.20 +struct
    3.21 +
    3.22 +val running_execs =
    3.23 +  Synchronized.var "Exec.running_execs" (Inttab.empty: {stable: bool} Inttab.table);
    3.24 +
    3.25 +fun is_stable exec_id =
    3.26 +  not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id))) andalso
    3.27 +  (case Inttab.lookup (Synchronized.value running_execs) exec_id of
    3.28 +    NONE => true
    3.29 +  | SOME {stable} => stable);
    3.30 +
    3.31 +fun running exec_id =
    3.32 +  Synchronized.change running_execs (Inttab.update_new (exec_id, {stable = true}));
    3.33 +
    3.34 +fun finished exec_id =
    3.35 +  Synchronized.change running_execs (Inttab.delete exec_id);
    3.36 +
    3.37 +fun canceled exec_id =
    3.38 +  Synchronized.change running_execs (Inttab.update (exec_id, {stable = false}));
    3.39 +
    3.40 +fun purge_unstable () =
    3.41 +  Synchronized.guarded_access running_execs
    3.42 +    (fn tab =>
    3.43 +      let
    3.44 +        val unstable = Inttab.fold (fn (exec_id, {stable = false}) => cons exec_id | _ => I) tab [];
    3.45 +        val tab' = fold Inttab.delete unstable tab;
    3.46 +      in SOME ((), tab') end);
    3.47 +
    3.48 +end;
    3.49 +

     4.1 --- a/src/Pure/PIDE/protocol.ML	Thu Jul 11 12:28:24 2013 +0200
     4.2 +++ b/src/Pure/PIDE/protocol.ML	Thu Jul 11 14:42:11 2013 +0200
     4.3 @@ -60,6 +60,7 @@
     4.4                |> YXML.string_of_body);
     4.5  
     4.6          val _ = List.app Future.cancel_group (Goal.reset_futures ());
     4.7 +        val _ = Exec.purge_unstable ();
     4.8          val _ = Isabelle_Process.reset_tracing ();
     4.9          val _ =
    4.10            Event_Timer.request (Time.+ (Time.now (), seconds 0.02))

     5.1 --- a/src/Pure/ROOT	Thu Jul 11 12:28:24 2013 +0200
     5.2 +++ b/src/Pure/ROOT	Thu Jul 11 14:42:11 2013 +0200
     5.3 @@ -150,6 +150,7 @@
     5.4      "ML/ml_syntax.ML"
     5.5      "ML/ml_thms.ML"
     5.6      "PIDE/active.ML"
     5.7 +    "PIDE/exec.ML"
     5.8      "PIDE/command.ML"
     5.9      "PIDE/document.ML"
    5.10      "PIDE/document_id.ML"

     6.1 --- a/src/Pure/ROOT.ML	Thu Jul 11 12:28:24 2013 +0200
     6.2 +++ b/src/Pure/ROOT.ML	Thu Jul 11 14:42:11 2013 +0200
     6.3 @@ -267,6 +267,7 @@
     6.4  use "Isar/outer_syntax.ML";
     6.5  use "General/graph_display.ML";
     6.6  use "Thy/present.ML";
     6.7 +use "PIDE/exec.ML";
     6.8  use "PIDE/command.ML";
     6.9  use "Thy/thy_load.ML";
    6.10  use "Thy/thy_info.ML";