1.1 --- a/src/Pure/PIDE/command.ML Thu Jul 04 12:02:11 2013 +0200
1.2 +++ b/src/Pure/PIDE/command.ML Thu Jul 04 16:04:53 2013 +0200
1.3 @@ -13,16 +13,19 @@
1.4 val memo: (unit -> 'a) -> 'a memo
1.5 val memo_value: 'a -> 'a memo
1.6 val memo_eval: 'a memo -> 'a
1.7 + val memo_fork: Future.params -> 'a memo -> unit
1.8 val memo_result: 'a memo -> 'a
1.9 + val memo_stable: 'a memo -> bool
1.10 val read: span -> Toplevel.transition
1.11 - val eval: span -> Toplevel.transition ->
1.12 - Toplevel.state * {malformed: bool} -> {failed: bool} * (Toplevel.state * {malformed: bool})
1.13 - type print = {name: string, pri: int, pr: unit lazy}
1.14 - val print: Toplevel.state -> Toplevel.transition -> Toplevel.state -> print list
1.15 - type print_function =
1.16 - {old_state: Toplevel.state, tr: Toplevel.transition, state: Toplevel.state} ->
1.17 - (unit -> unit) option
1.18 - val print_function: string -> int -> print_function -> unit
1.19 + type eval_state =
1.20 + {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state}
1.21 + type eval = eval_state memo
1.22 + val no_eval: eval
1.23 + val eval: span -> Toplevel.transition -> eval_state -> eval_state
1.24 + type print_fn = Toplevel.transition -> Toplevel.state -> unit
1.25 + type print = {name: string, pri: int, print: unit memo}
1.26 + val print: string -> eval -> print list
1.27 + val print_function: {name: string, pri: int} -> (string -> print_fn option) -> unit
1.28 end;
1.29
1.30 structure Command: COMMAND =
1.31 @@ -59,11 +62,21 @@
1.32 in SOME (res, Result res) end))
1.33 |> Exn.release;
1.34
1.35 +fun memo_fork params (Memo v) =
1.36 + (case Synchronized.value v of
1.37 + Result _ => ()
1.38 + | _ => ignore ((singleton o Future.forks) params (fn () => memo_eval (Memo v))));
1.39 +
1.40 fun memo_result (Memo v) =
1.41 (case Synchronized.value v of
1.42 Result res => Exn.release res
1.43 | _ => raise Fail "Unfinished memo result");
1.44
1.45 +fun memo_stable (Memo v) =
1.46 + (case Synchronized.value v of
1.47 + Expr _ => true
1.48 + | Result res => not (Exn.is_interrupt_exn res));
1.49 +
1.50 end;
1.51
1.52
1.53 @@ -98,6 +111,14 @@
1.54
1.55 (* eval *)
1.56
1.57 +type eval_state =
1.58 + {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state};
1.59 +val no_eval_state: eval_state =
1.60 + {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel};
1.61 +
1.62 +type eval = eval_state memo;
1.63 +val no_eval = memo_value no_eval_state;
1.64 +
1.65 local
1.66
1.67 fun run int tr st =
1.68 @@ -120,9 +141,9 @@
1.69
1.70 in
1.71
1.72 -fun eval span tr (st, {malformed}) =
1.73 +fun eval span tr ({malformed, state = st, ...}: eval_state) =
1.74 if malformed then
1.75 - ({failed = true}, (Toplevel.toplevel, {malformed = malformed}))
1.76 + {failed = true, malformed = malformed, command = tr, state = Toplevel.toplevel}
1.77 else
1.78 let
1.79 val malformed' = Toplevel.is_malformed tr;
1.80 @@ -142,11 +163,11 @@
1.81 let
1.82 val _ = if null errs then Exn.interrupt () else ();
1.83 val _ = Toplevel.status tr Markup.failed;
1.84 - in ({failed = true}, (st, {malformed = malformed'})) end
1.85 + in {failed = true, malformed = malformed', command = tr, state = st} end
1.86 | SOME st' =>
1.87 let
1.88 val _ = proof_status tr st';
1.89 - in ({failed = false}, (st', {malformed = malformed'})) end)
1.90 + in {failed = false, malformed = malformed', command = tr, state = st'} end)
1.91 end;
1.92
1.93 end;
1.94 @@ -154,16 +175,13 @@
1.95
1.96 (* print *)
1.97
1.98 -type print_function =
1.99 - {old_state: Toplevel.state, tr: Toplevel.transition, state: Toplevel.state} ->
1.100 - (unit -> unit) option;
1.101 -
1.102 -type print = {name: string, pri: int, pr: unit lazy};
1.103 +type print = {name: string, pri: int, print: unit memo};
1.104 +type print_fn = Toplevel.transition -> Toplevel.state -> unit;
1.105
1.106 local
1.107
1.108 -val print_functions =
1.109 - Synchronized.var "Command.print_functions" ([]: (string * (int * print_function)) list);
1.110 +type print_function = string * (int * (string -> print_fn option));
1.111 +val print_functions = Synchronized.var "Command.print_functions" ([]: print_function list);
1.112
1.113 fun output_error tr exn =
1.114 List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
1.115 @@ -174,14 +192,20 @@
1.116
1.117 in
1.118
1.119 -fun print st tr st' =
1.120 - rev (Synchronized.value print_functions) |> map_filter (fn (name, (pri, f)) =>
1.121 - (case Exn.capture (Runtime.controlled_execution f) {old_state = st, tr = tr, state = st'} of
1.122 +fun print command_name eval =
1.123 + rev (Synchronized.value print_functions) |> map_filter (fn (name, (pri, get_print_fn)) =>
1.124 + (case Exn.capture (Runtime.controlled_execution get_print_fn) command_name of
1.125 Exn.Res NONE => NONE
1.126 - | Exn.Res (SOME pr) => SOME {name = name, pri = pri, pr = (Lazy.lazy o print_error tr) pr}
1.127 - | Exn.Exn exn => SOME {name = name, pri = pri, pr = Lazy.lazy (fn () => output_error tr exn)}));
1.128 + | Exn.Res (SOME print_fn) =>
1.129 + SOME {name = name, pri = pri,
1.130 + print = memo (fn () =>
1.131 + let val {failed, command = tr, state = st', ...} = memo_result eval
1.132 + in if failed then () else print_error tr (fn () => print_fn tr st') () end)}
1.133 + | Exn.Exn exn =>
1.134 + SOME {name = name, pri = pri,
1.135 + print = memo (fn () => output_error (#command (memo_result eval)) exn)}));
1.136
1.137 -fun print_function name pri f =
1.138 +fun print_function {name, pri} f =
1.139 Synchronized.change print_functions (fn funs =>
1.140 (if not (AList.defined (op =) funs name) then ()
1.141 else warning ("Redefining command print function: " ^ quote name);
1.142 @@ -189,14 +213,15 @@
1.143
1.144 end;
1.145
1.146 -val _ = print_function "print_state" 0 (fn {tr, state, ...} =>
1.147 - let
1.148 - val is_init = Toplevel.is_init tr;
1.149 - val is_proof = Keyword.is_proof (Toplevel.name_of tr);
1.150 - val do_print =
1.151 - not is_init andalso
1.152 - (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof state));
1.153 - in if do_print then SOME (fn () => Toplevel.print_state false state) else NONE end);
1.154 +val _ =
1.155 + print_function {name = "print_state", pri = 0} (fn command_name => SOME (fn tr => fn st' =>
1.156 + let
1.157 + val is_init = Keyword.is_theory_begin command_name;
1.158 + val is_proof = Keyword.is_proof command_name;
1.159 + val do_print =
1.160 + not is_init andalso
1.161 + (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
1.162 + in if do_print then Toplevel.print_state false st' else () end));
1.163
1.164 end;
1.165
2.1 --- a/src/Pure/PIDE/document.ML Thu Jul 04 12:02:11 2013 +0200
2.2 +++ b/src/Pure/PIDE/document.ML Thu Jul 04 16:04:53 2013 +0200
2.3 @@ -56,23 +56,31 @@
2.4 fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ print_id id);
2.5
2.6
2.7 +(* command execution *)
2.8 +
2.9 +type exec = exec_id * (Command.eval * Command.print list); (*eval/print process*)
2.10 +val no_exec: exec = (no_id, (Command.no_eval, []));
2.11 +
2.12 +fun exec_result ((_, (eval, _)): exec) = Command.memo_result eval;
2.13 +
2.14 +fun exec_run ((_, (eval, prints)): exec) =
2.15 + (Command.memo_eval eval;
2.16 + prints |> List.app (fn {name, pri, print} =>
2.17 + Command.memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} print));
2.18 +
2.19 +
2.20
2.21 (** document structure **)
2.22
2.23 type node_header = string * Thy_Header.header * string list;
2.24 -type perspective = (command_id -> bool) * command_id option;
2.25 +type perspective = Inttab.set * command_id option;
2.26 structure Entries = Linear_Set(type key = command_id val ord = int_ord);
2.27
2.28 -type exec = ((Toplevel.state * {malformed: bool}) * Command.print list) Command.memo;
2.29 - (*eval/print process*)
2.30 -val no_exec =
2.31 - Command.memo_value ((Toplevel.toplevel, {malformed = false}), []: Command.print list);
2.32 -
2.33 abstype node = Node of
2.34 {header: node_header, (*master directory, theory header, errors*)
2.35 perspective: perspective, (*visible commands, last visible command*)
2.36 - entries: (exec_id * exec) option Entries.T * bool, (*command entries with excecutions, stable*)
2.37 - result: exec option} (*result of last execution*)
2.38 + entries: exec option Entries.T * bool, (*command entries with excecutions, stable*)
2.39 + result: Command.eval option} (*result of last execution*)
2.40 and version = Version of node String_Graph.T (*development graph wrt. static imports*)
2.41 with
2.42
2.43 @@ -83,7 +91,7 @@
2.44 make_node (f (header, perspective, entries, result));
2.45
2.46 fun make_perspective command_ids : perspective =
2.47 - (Inttab.defined (Inttab.make (map (rpair ()) command_ids)), try List.last command_ids);
2.48 + (Inttab.make_set command_ids, try List.last command_ids);
2.49
2.50 val no_header = ("", Thy_Header.make ("", Position.none) [] [], ["Bad theory header"]);
2.51 val no_perspective = make_perspective [];
2.52 @@ -112,7 +120,8 @@
2.53 fun set_perspective ids =
2.54 map_node (fn (header, _, entries, result) => (header, make_perspective ids, entries, result));
2.55
2.56 -val visible_command = #1 o get_perspective;
2.57 +val visible_commands = #1 o get_perspective;
2.58 +val visible_command = Inttab.defined o visible_commands;
2.59 val visible_last = #2 o get_perspective;
2.60 val visible_node = is_some o visible_last
2.61
2.62 @@ -164,8 +173,8 @@
2.63 NONE => err_undef "command entry" id
2.64 | SOME (exec, _) => exec);
2.65
2.66 -fun the_default_entry node (SOME id) = (id, the_default (no_id, no_exec) (the_entry node id))
2.67 - | the_default_entry _ NONE = (no_id, (no_id, no_exec));
2.68 +fun the_default_entry node (SOME id) = (id, the_default no_exec (the_entry node id))
2.69 + | the_default_entry _ NONE = (no_id, no_exec);
2.70
2.71 fun update_entry id exec =
2.72 map_entries (Entries.update (id, exec));
2.73 @@ -304,15 +313,14 @@
2.74
2.75 (* consolidated states *)
2.76
2.77 -fun stable_command (exec_id, exec) =
2.78 +fun stable_command ((exec_id, (eval, prints)): exec) =
2.79 not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id))) andalso
2.80 - (case Exn.capture Command.memo_result exec of
2.81 - Exn.Exn exn => not (Exn.is_interrupt exn)
2.82 - | Exn.Res _ => true);
2.83 + Command.memo_stable eval andalso
2.84 + forall (Command.memo_stable o #print) prints;
2.85
2.86 fun finished_theory node =
2.87 (case Exn.capture (Command.memo_result o the) (get_result node) of
2.88 - Exn.Res ((st, _), _) => can (Toplevel.end_theory Position.none) st
2.89 + Exn.Res {state = st, ...} => can (Toplevel.end_theory Position.none) st
2.90 | _ => false);
2.91
2.92
2.93 @@ -325,15 +333,7 @@
2.94
2.95 fun start_execution state =
2.96 let
2.97 - fun execute exec =
2.98 - Command.memo_eval exec
2.99 - |> (fn (_, print) =>
2.100 - print |> List.app (fn {name, pri, pr} =>
2.101 - Lazy.future {name = name, group = NONE, deps = [], pri = pri, interrupts = true} pr
2.102 - |> ignore));
2.103 -
2.104 val (version_id, group, running) = execution_of state;
2.105 -
2.106 val _ =
2.107 (singleton o Future.forks)
2.108 {name = "Document.execution", group = SOME group, deps = [], pri = ~2, interrupts = true}
2.109 @@ -350,7 +350,7 @@
2.110 (fn () =>
2.111 iterate_entries (fn (_, opt_exec) => fn () =>
2.112 (case opt_exec of
2.113 - SOME (_, exec) => if ! running then SOME (execute exec) else NONE
2.114 + SOME exec => if ! running then SOME (exec_run exec) else NONE
2.115 | NONE => NONE)) node ()))));
2.116 in () end;
2.117
2.118 @@ -391,10 +391,10 @@
2.119 SOME thy => thy
2.120 | NONE =>
2.121 Toplevel.end_theory (Position.file_only import)
2.122 - (fst (fst
2.123 + (#state
2.124 (Command.memo_result
2.125 - (the_default no_exec
2.126 - (get_result (snd (the (AList.lookup (op =) deps import))))))))));
2.127 + (the_default Command.no_eval
2.128 + (get_result (snd (the (AList.lookup (op =) deps import)))))))));
2.129 val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
2.130 in Thy_Load.begin_theory master_dir header parents end;
2.131
2.132 @@ -439,28 +439,28 @@
2.133 else
2.134 let
2.135 val (name, span) = the_command state command_id' ||> Lazy.force;
2.136 +
2.137 fun illegal_init _ = error "Illegal theory header after end of theory";
2.138 val (modify_init, init') =
2.139 if Keyword.is_theory_begin name then
2.140 (Toplevel.modify_init (fn () => the_default illegal_init init span), NONE)
2.141 else (I, init);
2.142 +
2.143 val exec_id' = new_id ();
2.144 - val exec_id'_string = print_id exec_id';
2.145 - val read =
2.146 - Position.setmp_thread_data (Position.id_only exec_id'_string)
2.147 - (fn () =>
2.148 - Command.read span
2.149 - |> modify_init
2.150 - |> Toplevel.put_id exec_id'_string);
2.151 - val exec' =
2.152 + val eval' =
2.153 Command.memo (fn () =>
2.154 let
2.155 - val ((st, malformed), _) = Command.memo_result (snd (snd command_exec));
2.156 - val tr = read ();
2.157 - val ({failed}, (st', malformed')) = Command.eval span tr (st, malformed);
2.158 - val print = if failed orelse not command_visible then [] else Command.print st tr st';
2.159 - in ((st', malformed'), print) end);
2.160 - val command_exec' = (command_id', (exec_id', exec'));
2.161 + val eval_state = exec_result (snd command_exec);
2.162 + val tr =
2.163 + Position.setmp_thread_data (Position.id_only (print_id exec_id'))
2.164 + (fn () =>
2.165 + Command.read span
2.166 + |> modify_init
2.167 + |> Toplevel.put_id (print_id exec_id')) ();
2.168 + in Command.eval span tr eval_state end);
2.169 + val prints' = if command_visible then Command.print name eval' else [];
2.170 +
2.171 + val command_exec' = (command_id', (exec_id', (eval', prints')));
2.172 in SOME (command_exec' :: execs, command_exec', init') end;
2.173
2.174 in
2.175 @@ -502,7 +502,7 @@
2.176 else last_common state last_visible node0 node;
2.177 val common_command_exec = the_default_entry node common;
2.178
2.179 - val (new_execs, (command_id', (_, exec')), _) =
2.180 + val (new_execs, (command_id', (_, (eval', _))), _) =
2.181 ([], common_command_exec, if initial then SOME init else NONE) |>
2.182 (still_visible orelse node_required) ?
2.183 iterate_entries_after common
2.184 @@ -514,13 +514,14 @@
2.185 iterate_entries_after common
2.186 (fn ((_, id0), exec0) => fn res =>
2.187 if is_none exec0 then NONE
2.188 - else if exists (fn (_, (id, _)) => id0 = id) new_execs then SOME res
2.189 + else if exists (fn (_, (id, _)) => id0 = id) new_execs
2.190 + then SOME res
2.191 else SOME (id0 :: res)) node0 [];
2.192
2.193 val last_exec = if command_id' = no_id then NONE else SOME command_id';
2.194 val result =
2.195 if is_some (after_entry node last_exec) then NONE
2.196 - else SOME exec';
2.197 + else SOME eval';
2.198
2.199 val node' = node
2.200 |> fold reset_entry no_execs