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