1.1 --- a/src/Pure/PIDE/command.ML Thu Jul 11 16:01:48 2013 +0200
1.2 +++ b/src/Pure/PIDE/command.ML Thu Jul 11 16:26:14 2013 +0200
1.3 @@ -6,25 +6,21 @@
1.4
1.5 signature COMMAND =
1.6 sig
1.7 - type eval_process
1.8 - type eval = {exec_id: Document_ID.exec, eval_process: eval_process}
1.9 + val read: (unit -> theory) -> Token.T list -> Toplevel.transition
1.10 + type eval
1.11 val eval_result_state: eval -> Toplevel.state
1.12 val eval_same: eval * eval -> bool
1.13 - type print_process
1.14 - type print =
1.15 - {name: string, pri: int, persistent: bool,
1.16 - exec_id: Document_ID.exec, print_process: print_process}
1.17 - type exec = eval * print list
1.18 - val no_exec: exec
1.19 - val exec_ids: exec option -> Document_ID.exec list
1.20 - val read: (unit -> theory) -> Token.T list -> Toplevel.transition
1.21 val eval: (unit -> theory) -> Token.T list -> eval -> eval
1.22 + type print
1.23 val print: bool -> string -> eval -> print list -> print list option
1.24 type print_fn = Toplevel.transition -> Toplevel.state -> unit
1.25 val print_function: {name: string, pri: int, persistent: bool} ->
1.26 ({command_name: string} -> print_fn option) -> unit
1.27 val no_print_function: string -> unit
1.28 - val execute: exec -> unit
1.29 + type exec = eval * print list
1.30 + val no_exec: exec
1.31 + val exec_ids: exec option -> Document_ID.exec list
1.32 + val exec: exec -> unit
1.33 end;
1.34
1.35 structure Command: COMMAND =
1.36 @@ -78,34 +74,6 @@
1.37
1.38 (** main phases of execution **)
1.39
1.40 -(* type definitions *)
1.41 -
1.42 -type eval_state =
1.43 - {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state};
1.44 -val init_eval_state =
1.45 - {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel};
1.46 -
1.47 -type eval_process = eval_state memo;
1.48 -type eval = {exec_id: Document_ID.exec, eval_process: eval_process};
1.49 -
1.50 -fun eval_result ({eval_process, ...}: eval) = memo_result eval_process;
1.51 -val eval_result_state = #state o eval_result;
1.52 -
1.53 -fun eval_same ({exec_id, ...}: eval, {exec_id = exec_id', ...}: eval) =
1.54 - exec_id = exec_id' andalso Exec.is_stable exec_id;
1.55 -
1.56 -type print_process = unit memo;
1.57 -type print =
1.58 - {name: string, pri: int, persistent: bool,
1.59 - exec_id: Document_ID.exec, print_process: print_process};
1.60 -
1.61 -type exec = eval * print list;
1.62 -val no_exec: exec = ({exec_id = Document_ID.none, eval_process = memo_value init_eval_state}, []);
1.63 -
1.64 -fun exec_ids (NONE: exec option) = []
1.65 - | exec_ids (SOME ({exec_id, ...}, prints)) = exec_id :: map #exec_id prints;
1.66 -
1.67 -
1.68 (* read *)
1.69
1.70 fun read init span =
1.71 @@ -138,6 +106,19 @@
1.72
1.73 (* eval *)
1.74
1.75 +type eval_state =
1.76 + {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state};
1.77 +val init_eval_state =
1.78 + {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel};
1.79 +
1.80 +datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state memo};
1.81 +
1.82 +fun eval_result (Eval {eval_process, ...}) = memo_result eval_process;
1.83 +val eval_result_state = #state o eval_result;
1.84 +
1.85 +fun eval_same (Eval {exec_id, ...}, Eval {exec_id = exec_id', ...}) =
1.86 + exec_id = exec_id' andalso Exec.is_stable exec_id;
1.87 +
1.88 local
1.89
1.90 fun run int tr st =
1.91 @@ -198,13 +179,17 @@
1.92 Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id))
1.93 (fn () => read init span |> Toplevel.exec_id exec_id) ();
1.94 in eval_state span tr (eval_result eval0) end;
1.95 - in {exec_id = exec_id, eval_process = memo exec_id process} end;
1.96 + in Eval {exec_id = exec_id, eval_process = memo exec_id process} end;
1.97
1.98 end;
1.99
1.100
1.101 (* print *)
1.102
1.103 +datatype print = Print of
1.104 + {name: string, pri: int, persistent: bool,
1.105 + exec_id: Document_ID.exec, print_process: unit memo};
1.106 +
1.107 type print_fn = Toplevel.transition -> Toplevel.state -> unit;
1.108
1.109 local
1.110 @@ -216,7 +201,9 @@
1.111 (Toplevel.setmp_thread_position tr o Runtime.controlled_execution) e () handle exn =>
1.112 List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
1.113
1.114 -fun print_stable (print: print) = Exec.is_stable (#exec_id print);
1.115 +fun print_persistent (Print {persistent, ...}) = persistent;
1.116 +fun print_stable (Print {exec_id, ...}) = Exec.is_stable exec_id;
1.117 +fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id';
1.118
1.119 in
1.120
1.121 @@ -236,8 +223,9 @@
1.122 else print_error tr (fn () => print_fn tr st')
1.123 end;
1.124 in
1.125 - {name = name, pri = pri, persistent = persistent,
1.126 - exec_id = exec_id, print_process = memo exec_id process}
1.127 + Print {
1.128 + name = name, pri = pri, persistent = persistent,
1.129 + exec_id = exec_id, print_process = memo exec_id process}
1.130 end;
1.131 in
1.132 (case Exn.capture (Runtime.controlled_execution get_fn) {command_name = command_name} of
1.133 @@ -249,13 +237,12 @@
1.134 val new_prints =
1.135 if command_visible then
1.136 rev (Synchronized.value print_functions) |> map_filter (fn pr =>
1.137 - (case find_first (equal (fst pr) o #name) old_prints of
1.138 + (case find_first (fn Print {name, ...} => name = fst pr) old_prints of
1.139 SOME print => if print_stable print then SOME print else new_print pr
1.140 | NONE => new_print pr))
1.141 - else filter (fn print => #persistent print andalso print_stable print) old_prints;
1.142 + else filter (fn print => print_persistent print andalso print_stable print) old_prints;
1.143 in
1.144 - if eq_list (op = o pairself #exec_id) (old_prints, new_prints) then NONE
1.145 - else SOME new_prints
1.146 + if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints
1.147 end;
1.148
1.149 fun print_function {name, pri, persistent} f =
1.150 @@ -281,15 +268,29 @@
1.151 in if do_print then Toplevel.print_state false st' else () end));
1.152
1.153
1.154 -(* combined execution process *)
1.155 +(* combined execution *)
1.156
1.157 -fun run_print ({name, pri, print_process, ...}: print) =
1.158 +type exec = eval * print list;
1.159 +val no_exec: exec =
1.160 + (Eval {exec_id = Document_ID.none, eval_process = memo_value init_eval_state}, []);
1.161 +
1.162 +fun exec_ids NONE = []
1.163 + | exec_ids (SOME (Eval {exec_id, ...}, prints)) =
1.164 + exec_id :: map (fn Print {exec_id, ...} => exec_id) prints;
1.165 +
1.166 +local
1.167 +
1.168 +fun run_print (Print {name, pri, print_process, ...}) =
1.169 (if Multithreading.enabled () then
1.170 memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true}
1.171 else memo_exec) print_process;
1.172
1.173 -fun execute (({eval_process, ...}, prints): exec) =
1.174 +in
1.175 +
1.176 +fun exec (Eval {eval_process, ...}, prints) =
1.177 (memo_exec eval_process; List.app run_print prints);
1.178
1.179 end;
1.180
1.181 +end;
1.182 +