1.1 --- a/src/Pure/PIDE/command.ML Fri Jul 05 17:09:28 2013 +0200
1.2 +++ b/src/Pure/PIDE/command.ML Fri Jul 05 18:37:44 2013 +0200
1.3 @@ -1,36 +1,26 @@
1.4 (* Title: Pure/PIDE/command.ML
1.5 Author: Makarius
1.6
1.7 -Prover command execution.
1.8 +Prover command execution: read -- eval -- print.
1.9 *)
1.10
1.11 signature COMMAND =
1.12 sig
1.13 - type span = Token.T list
1.14 - val range: span -> Position.range
1.15 - val proper_range: span -> Position.range
1.16 - type 'a memo
1.17 - val memo: (unit -> 'a) -> 'a memo
1.18 - val memo_value: 'a -> 'a memo
1.19 - val memo_eval: 'a memo -> 'a
1.20 - val memo_fork: Future.params -> 'a memo -> unit
1.21 - val memo_result: 'a memo -> 'a
1.22 - val memo_stable: 'a memo -> bool
1.23 - val read: span -> Toplevel.transition
1.24 - type eval_state =
1.25 - {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state}
1.26 - type eval = {exec_id: Document_ID.exec, eval: eval_state memo}
1.27 + type span
1.28 + type eval_process
1.29 + type eval = {exec_id: Document_ID.exec, eval_process: eval_process}
1.30 + type print_process
1.31 + type print = {name: string, pri: int, exec_id: Document_ID.exec, print_process: print_process}
1.32 + type exec = eval * print list
1.33 + val read: (unit -> theory) -> span -> Toplevel.transition
1.34 val no_eval: eval
1.35 - val eval_result: eval -> eval_state
1.36 - val eval: span -> Toplevel.transition -> eval_state -> eval_state
1.37 + val eval_result_state: eval -> Toplevel.state
1.38 + val eval: (unit -> theory) -> span -> eval -> eval
1.39 + val print: string -> eval -> print list
1.40 type print_fn = Toplevel.transition -> Toplevel.state -> unit
1.41 - type print = {name: string, pri: int, exec_id: Document_ID.exec, print: unit memo}
1.42 - val print: string -> eval -> print list
1.43 val print_function: {name: string, pri: int} -> (string -> print_fn option) -> unit
1.44 - type exec = eval * print list
1.45 val no_exec: exec
1.46 val exec_ids: exec -> Document_ID.exec list
1.47 - val exec_result: exec -> eval_state
1.48 val exec_run: exec -> unit
1.49 val stable_eval: eval -> bool
1.50 val stable_print: print -> bool
1.51 @@ -39,15 +29,7 @@
1.52 structure Command: COMMAND =
1.53 struct
1.54
1.55 -(* source *)
1.56 -
1.57 -type span = Token.T list;
1.58 -
1.59 -val range = Token.position_range_of;
1.60 -val proper_range = Token.position_range_of o #1 o take_suffix Token.is_improper;
1.61 -
1.62 -
1.63 -(* memo results *)
1.64 +(** memo results -- including physical interrupts! **)
1.65
1.66 datatype 'a expr =
1.67 Expr of unit -> 'a |
1.68 @@ -66,7 +48,7 @@
1.69 Synchronized.guarded_access v
1.70 (fn Result res => SOME (res, Result res)
1.71 | Expr e =>
1.72 - let val res = Exn.capture e (); (*memoing of physical interrupts!*)
1.73 + let val res = Exn.capture e (); (*sic!*)
1.74 in SOME (res, Result res) end))
1.75 |> Exn.release;
1.76
1.77 @@ -88,16 +70,29 @@
1.78 end;
1.79
1.80
1.81 -(** main phases: read -- eval -- print **)
1.82 +
1.83 +(** main phases **)
1.84 +
1.85 +type span = Token.T list
1.86 +
1.87 +type eval_state =
1.88 + {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state};
1.89 +type eval_process = eval_state memo;
1.90 +type eval = {exec_id: Document_ID.exec, eval_process: eval_process};
1.91 +
1.92 +type print_process = unit memo;
1.93 +type print = {name: string, pri: int, exec_id: Document_ID.exec, print_process: print_process};
1.94 +
1.95
1.96 (* read *)
1.97
1.98 -fun read span =
1.99 +fun read init span =
1.100 let
1.101 val outer_syntax = #2 (Outer_Syntax.get_syntax ());
1.102 val command_reports = Outer_Syntax.command_reports outer_syntax;
1.103
1.104 - val proper_range = Position.set_range (proper_range span);
1.105 + val proper_range =
1.106 + Position.set_range (Token.position_range_of (#1 (take_suffix Token.is_improper span)));
1.107 val pos =
1.108 (case find_first Token.is_command span of
1.109 SOME tok => Token.position_of tok
1.110 @@ -112,8 +107,8 @@
1.111 [tr] =>
1.112 if Keyword.is_control (Toplevel.name_of tr) then
1.113 Toplevel.malformed pos "Illegal control command"
1.114 - else tr
1.115 - | [] => Toplevel.ignored (Position.set_range (range span))
1.116 + else Toplevel.modify_init init tr
1.117 + | [] => Toplevel.ignored (Position.set_range (Token.position_range_of span))
1.118 | _ => Toplevel.malformed proper_range "Exactly one command expected")
1.119 handle ERROR msg => Toplevel.malformed proper_range msg
1.120 end;
1.121 @@ -121,15 +116,13 @@
1.122
1.123 (* eval *)
1.124
1.125 -type eval_state =
1.126 - {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state};
1.127 val no_eval_state: eval_state =
1.128 {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel};
1.129
1.130 -type eval = {exec_id: Document_ID.exec, eval: eval_state memo};
1.131 +val no_eval: eval = {exec_id = Document_ID.none, eval_process = memo_value no_eval_state};
1.132
1.133 -val no_eval: eval = {exec_id = Document_ID.none, eval = memo_value no_eval_state};
1.134 -fun eval_result ({eval, ...}: eval) = memo_result eval;
1.135 +fun eval_result ({eval_process, ...}: eval) = memo_result eval_process;
1.136 +val eval_result_state = #state o eval_result;
1.137
1.138 local
1.139
1.140 @@ -151,9 +144,7 @@
1.141 SOME prf => Toplevel.status tr (Proof.status_markup prf)
1.142 | NONE => ());
1.143
1.144 -in
1.145 -
1.146 -fun eval span tr ({malformed, state = st, ...}: eval_state) =
1.147 +fun eval_state span tr ({malformed, state = st, ...}: eval_state) =
1.148 if malformed then
1.149 {failed = true, malformed = malformed, command = tr, state = Toplevel.toplevel}
1.150 else
1.151 @@ -182,12 +173,24 @@
1.152 in {failed = false, malformed = malformed', command = tr, state = st'} end)
1.153 end;
1.154
1.155 +in
1.156 +
1.157 +fun eval init span eval0 =
1.158 + let
1.159 + val exec_id = Document_ID.make ();
1.160 + fun process () =
1.161 + let
1.162 + val tr =
1.163 + Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id))
1.164 + (fn () => read init span |> Toplevel.put_id exec_id) ();
1.165 + in eval_state span tr (eval_result eval0) end;
1.166 + in {exec_id = exec_id, eval_process = memo process} end;
1.167 +
1.168 end;
1.169
1.170
1.171 (* print *)
1.172
1.173 -type print = {name: string, pri: int, exec_id: Document_ID.exec, print: unit memo};
1.174 type print_fn = Toplevel.transition -> Toplevel.state -> unit;
1.175
1.176 local
1.177 @@ -211,21 +214,21 @@
1.178 | Exn.Res (SOME print_fn) =>
1.179 let
1.180 val exec_id = Document_ID.make ();
1.181 - fun body () =
1.182 + fun process () =
1.183 let
1.184 val {failed, command, state = st', ...} = eval_result eval;
1.185 val tr = Toplevel.put_id exec_id command;
1.186 in if failed then () else print_error tr (fn () => print_fn tr st') () end;
1.187 - in SOME {name = name, pri = pri, exec_id = exec_id, print = memo body} end
1.188 + in SOME {name = name, pri = pri, exec_id = exec_id, print_process = memo process} end
1.189 | Exn.Exn exn =>
1.190 let
1.191 val exec_id = Document_ID.make ();
1.192 - fun body () =
1.193 + fun process () =
1.194 let
1.195 val {command, ...} = eval_result eval;
1.196 val tr = Toplevel.put_id exec_id command;
1.197 in output_error tr exn end;
1.198 - in SOME {name = name, pri = pri, exec_id = exec_id, print = memo body} end));
1.199 + in SOME {name = name, pri = pri, exec_id = exec_id, print_process = memo process} end));
1.200
1.201 fun print_function {name, pri} f =
1.202 Synchronized.change print_functions (fn funs =>
1.203 @@ -256,12 +259,10 @@
1.204
1.205 fun exec_ids (({exec_id, ...}, prints): exec) = exec_id :: map #exec_id prints;
1.206
1.207 -fun exec_result (({eval, ...}, _): exec) = memo_result eval;
1.208 -
1.209 -fun exec_run (({eval, ...}, prints): exec) =
1.210 - (memo_eval eval;
1.211 - prints |> List.app (fn {name, pri, print, ...} =>
1.212 - memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} print));
1.213 +fun exec_run (({eval_process, ...}, prints): exec) =
1.214 + (memo_eval eval_process;
1.215 + prints |> List.app (fn {name, pri, print_process, ...} =>
1.216 + memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} print_process));
1.217
1.218
1.219 (* stable situations after cancellation *)
1.220 @@ -269,11 +270,11 @@
1.221 fun stable_goals exec_id =
1.222 not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id)));
1.223
1.224 -fun stable_eval ({exec_id, eval}: eval) =
1.225 - stable_goals exec_id andalso memo_stable eval;
1.226 +fun stable_eval ({exec_id, eval_process}: eval) =
1.227 + stable_goals exec_id andalso memo_stable eval_process;
1.228
1.229 -fun stable_print ({exec_id, print, ...}: print) =
1.230 - stable_goals exec_id andalso memo_stable print;
1.231 +fun stable_print ({exec_id, print_process, ...}: print) =
1.232 + stable_goals exec_id andalso memo_stable print_process;
1.233
1.234 end;
1.235
2.1 --- a/src/Pure/PIDE/document.ML Fri Jul 05 17:09:28 2013 +0200
2.2 +++ b/src/Pure/PIDE/document.ML Fri Jul 05 18:37:44 2013 +0200
2.3 @@ -109,8 +109,8 @@
2.4 map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result));
2.5
2.6 fun finished_theory node =
2.7 - (case Exn.capture (Command.eval_result o the) (get_result node) of
2.8 - Exn.Res {state = st, ...} => can (Toplevel.end_theory Position.none) st
2.9 + (case Exn.capture (Command.eval_result_state o the) (get_result node) of
2.10 + Exn.Res st => can (Toplevel.end_theory Position.none) st
2.11 | _ => false);
2.12
2.13 fun get_node nodes name = String_Graph.get_node nodes name
2.14 @@ -347,10 +347,9 @@
2.15 SOME thy => thy
2.16 | NONE =>
2.17 Toplevel.end_theory (Position.file_only import)
2.18 - (#state
2.19 - (Command.eval_result
2.20 - (the_default Command.no_eval
2.21 - (get_result (snd (the (AList.lookup (op =) deps import)))))))));
2.22 + (Command.eval_result_state
2.23 + (the_default Command.no_eval
2.24 + (get_result (snd (the (AList.lookup (op =) deps import))))))));
2.25 val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
2.26 in Thy_Load.begin_theory master_dir header parents end;
2.27
2.28 @@ -391,31 +390,16 @@
2.29 else (common, flags)
2.30 end;
2.31
2.32 +fun illegal_init _ = error "Illegal theory header after end of theory";
2.33 +
2.34 fun new_exec state proper_init command_visible command_id' (execs, command_exec, init) =
2.35 if not proper_init andalso is_none init then NONE
2.36 else
2.37 let
2.38 + val (_, (eval, _)) = command_exec;
2.39 val (command_name, span) = the_command state command_id' ||> Lazy.force;
2.40 -
2.41 - fun illegal_init _ = error "Illegal theory header after end of theory";
2.42 - val (modify_init, init') =
2.43 - if Keyword.is_theory_begin command_name then
2.44 - (Toplevel.modify_init (fn () => the_default illegal_init init span), NONE)
2.45 - else (I, init);
2.46 -
2.47 - val exec_id' = Document_ID.make ();
2.48 - val eval_body' =
2.49 - Command.memo (fn () =>
2.50 - let
2.51 - val eval_state = Command.exec_result (snd command_exec);
2.52 - val tr =
2.53 - Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id'))
2.54 - (fn () =>
2.55 - Command.read span
2.56 - |> modify_init
2.57 - |> Toplevel.put_id exec_id') ();
2.58 - in Command.eval span tr eval_state end);
2.59 - val eval' = {exec_id = exec_id', eval = eval_body'};
2.60 + val init' = if Keyword.is_theory_begin command_name then NONE else init;
2.61 + val eval' = Command.eval (fn () => the_default illegal_init init span) span eval;
2.62 val prints' = if command_visible then Command.print command_name eval' else [];
2.63 val command_exec' = (command_id', (eval', prints'));
2.64 in SOME (command_exec' :: execs, command_exec', init') end;
3.1 --- a/src/Pure/Thy/thy_load.ML Fri Jul 05 17:09:28 2013 +0200
3.2 +++ b/src/Pure/Thy/thy_load.ML Fri Jul 05 18:37:44 2013 +0200
3.3 @@ -217,8 +217,7 @@
3.4 let
3.5 fun prepare_span span =
3.6 Thy_Syntax.span_content span
3.7 - |> Command.read
3.8 - |> Toplevel.modify_init init
3.9 + |> Command.read init
3.10 |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
3.11
3.12 fun element_result span_elem (st, _) =