1.1 --- a/src/Pure/PIDE/command.ML Fri Jul 05 16:22:28 2013 +0200
1.2 +++ b/src/Pure/PIDE/command.ML Fri Jul 05 17:09:28 2013 +0200
1.3 @@ -19,19 +19,20 @@
1.4 val read: span -> Toplevel.transition
1.5 type eval_state =
1.6 {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state}
1.7 - type eval = eval_state memo
1.8 + type eval = {exec_id: Document_ID.exec, eval: eval_state memo}
1.9 val no_eval: eval
1.10 + val eval_result: eval -> eval_state
1.11 val eval: span -> Toplevel.transition -> eval_state -> eval_state
1.12 type print_fn = Toplevel.transition -> Toplevel.state -> unit
1.13 type print = {name: string, pri: int, exec_id: Document_ID.exec, print: unit memo}
1.14 val print: string -> eval -> print list
1.15 val print_function: {name: string, pri: int} -> (string -> print_fn option) -> unit
1.16 - type exec = Document_ID.exec * (eval * print list)
1.17 + type exec = eval * print list
1.18 val no_exec: exec
1.19 val exec_ids: exec -> Document_ID.exec list
1.20 val exec_result: exec -> eval_state
1.21 val exec_run: exec -> unit
1.22 - val stable_eval: exec -> bool
1.23 + val stable_eval: eval -> bool
1.24 val stable_print: print -> bool
1.25 end;
1.26
1.27 @@ -125,8 +126,10 @@
1.28 val no_eval_state: eval_state =
1.29 {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel};
1.30
1.31 -type eval = eval_state memo;
1.32 -val no_eval = memo_value no_eval_state;
1.33 +type eval = {exec_id: Document_ID.exec, eval: eval_state memo};
1.34 +
1.35 +val no_eval: eval = {exec_id = Document_ID.none, eval = memo_value no_eval_state};
1.36 +fun eval_result ({eval, ...}: eval) = memo_result eval;
1.37
1.38 local
1.39
1.40 @@ -210,7 +213,7 @@
1.41 val exec_id = Document_ID.make ();
1.42 fun body () =
1.43 let
1.44 - val {failed, command, state = st', ...} = memo_result eval;
1.45 + val {failed, command, state = st', ...} = eval_result eval;
1.46 val tr = Toplevel.put_id exec_id command;
1.47 in if failed then () else print_error tr (fn () => print_fn tr st') () end;
1.48 in SOME {name = name, pri = pri, exec_id = exec_id, print = memo body} end
1.49 @@ -219,7 +222,7 @@
1.50 val exec_id = Document_ID.make ();
1.51 fun body () =
1.52 let
1.53 - val {command, ...} = memo_result eval;
1.54 + val {command, ...} = eval_result eval;
1.55 val tr = Toplevel.put_id exec_id command;
1.56 in output_error tr exn end;
1.57 in SOME {name = name, pri = pri, exec_id = exec_id, print = memo body} end));
1.58 @@ -244,29 +247,29 @@
1.59
1.60
1.61
1.62 -(** managed evaluation with potential interrupts **)
1.63 +(** managed evaluation **)
1.64
1.65 (* execution *)
1.66
1.67 -type exec = Document_ID.exec * (eval * print list);
1.68 -val no_exec: exec = (Document_ID.none, (no_eval, []));
1.69 +type exec = eval * print list;
1.70 +val no_exec: exec = (no_eval, []);
1.71
1.72 -fun exec_ids ((exec_id, (_, prints)): exec) = exec_id :: map #exec_id prints;
1.73 +fun exec_ids (({exec_id, ...}, prints): exec) = exec_id :: map #exec_id prints;
1.74
1.75 -fun exec_result ((_, (eval, _)): exec) = memo_result eval;
1.76 +fun exec_result (({eval, ...}, _): exec) = memo_result eval;
1.77
1.78 -fun exec_run ((_, (eval, prints)): exec) =
1.79 +fun exec_run (({eval, ...}, prints): exec) =
1.80 (memo_eval eval;
1.81 prints |> List.app (fn {name, pri, print, ...} =>
1.82 memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} print));
1.83
1.84
1.85 -(* stable situations *)
1.86 +(* stable situations after cancellation *)
1.87
1.88 fun stable_goals exec_id =
1.89 not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id)));
1.90
1.91 -fun stable_eval ((exec_id, (eval, _)): exec) =
1.92 +fun stable_eval ({exec_id, eval}: eval) =
1.93 stable_goals exec_id andalso memo_stable eval;
1.94
1.95 fun stable_print ({exec_id, print, ...}: print) =
2.1 --- a/src/Pure/PIDE/document.ML Fri Jul 05 16:22:28 2013 +0200
2.2 +++ b/src/Pure/PIDE/document.ML Fri Jul 05 17:09:28 2013 +0200
2.3 @@ -108,6 +108,11 @@
2.4 fun set_result result =
2.5 map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result));
2.6
2.7 +fun finished_theory node =
2.8 + (case Exn.capture (Command.eval_result o the) (get_result node) of
2.9 + Exn.Res {state = st, ...} => can (Toplevel.end_theory Position.none) st
2.10 + | _ => false);
2.11 +
2.12 fun get_node nodes name = String_Graph.get_node nodes name
2.13 handle String_Graph.UNDEF _ => empty_node;
2.14 fun default_node name = String_Graph.default_node (name, empty_node);
2.15 @@ -275,12 +280,6 @@
2.16 in (versions', commands', execution) end);
2.17
2.18
2.19 -fun finished_theory node =
2.20 - (case Exn.capture (Command.memo_result o the) (get_result node) of
2.21 - Exn.Res {state = st, ...} => can (Toplevel.end_theory Position.none) st
2.22 - | _ => false);
2.23 -
2.24 -
2.25
2.26 (** document execution **)
2.27
2.28 @@ -349,7 +348,7 @@
2.29 | NONE =>
2.30 Toplevel.end_theory (Position.file_only import)
2.31 (#state
2.32 - (Command.memo_result
2.33 + (Command.eval_result
2.34 (the_default Command.no_eval
2.35 (get_result (snd (the (AList.lookup (op =) deps import)))))))));
2.36 val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
2.37 @@ -376,11 +375,11 @@
2.38 val same' =
2.39 (case opt_exec of
2.40 NONE => false
2.41 - | SOME (exec_id, exec) =>
2.42 + | SOME (eval, _) =>
2.43 (case lookup_entry node0 id of
2.44 NONE => false
2.45 - | SOME (exec_id0, _) =>
2.46 - exec_id = exec_id0 andalso Command.stable_eval (exec_id, exec)));
2.47 + | SOME (eval0, _) =>
2.48 + #exec_id eval = #exec_id eval0 andalso Command.stable_eval eval));
2.49 in SOME (same', (prev, flags')) end
2.50 else NONE;
2.51 val (same, (common, flags)) =
2.52 @@ -405,7 +404,7 @@
2.53 else (I, init);
2.54
2.55 val exec_id' = Document_ID.make ();
2.56 - val eval' =
2.57 + val eval_body' =
2.58 Command.memo (fn () =>
2.59 let
2.60 val eval_state = Command.exec_result (snd command_exec);
2.61 @@ -416,13 +415,14 @@
2.62 |> modify_init
2.63 |> Toplevel.put_id exec_id') ();
2.64 in Command.eval span tr eval_state end);
2.65 + val eval' = {exec_id = exec_id', eval = eval_body'};
2.66 val prints' = if command_visible then Command.print command_name eval' else [];
2.67 - val command_exec' = (command_id', (exec_id', (eval', prints')));
2.68 + val command_exec' = (command_id', (eval', prints'));
2.69 in SOME (command_exec' :: execs, command_exec', init') end;
2.70
2.71 fun update_prints state node command_id =
2.72 (case the_entry node command_id of
2.73 - SOME (exec_id, (eval, prints)) =>
2.74 + SOME (eval, prints) =>
2.75 let
2.76 val (command_name, _) = the_command state command_id;
2.77 val new_prints = Command.print command_name eval;
2.78 @@ -433,7 +433,7 @@
2.79 | NONE => new_print));
2.80 in
2.81 if eq_list (op = o pairself #exec_id) (prints, prints') then NONE
2.82 - else SOME (command_id, (exec_id, (eval, prints')))
2.83 + else SOME (command_id, (eval, prints'))
2.84 end
2.85 | NONE => NONE);
2.86
2.87 @@ -479,7 +479,7 @@
2.88 else last_common state last_visible node0 node;
2.89 val common_command_exec = the_default_entry node common;
2.90
2.91 - val (new_execs, (command_id', (_, (eval', _))), _) =
2.92 + val (new_execs, (command_id', (eval', _)), _) =
2.93 ([], common_command_exec, if initial then SOME init else NONE) |>
2.94 (still_visible orelse node_required) ?
2.95 iterate_entries_after common
2.96 @@ -489,14 +489,14 @@
2.97
2.98 val updated_execs =
2.99 (visible_commands, new_execs) |-> Inttab.fold (fn (id, ()) =>
2.100 - if exists (fn (_, (id', _)) => id = id') new_execs then I
2.101 + if exists (fn (_, ({exec_id = id', ...}, _)) => id = id') new_execs then I
2.102 else append (the_list (update_prints state node id)));
2.103
2.104 val no_execs =
2.105 iterate_entries_after common
2.106 (fn ((_, id0), exec0) => fn res =>
2.107 if is_none exec0 then NONE
2.108 - else if exists (fn (_, (id, _)) => id0 = id) updated_execs
2.109 + else if exists (fn (_, ({exec_id = id, ...}, _)) => id0 = id) updated_execs
2.110 then SOME res
2.111 else SOME (id0 :: res)) node0 [];
2.112