1.1 --- a/src/Pure/PIDE/command.ML Mon Jul 29 13:00:36 2013 +0200
1.2 +++ b/src/Pure/PIDE/command.ML Mon Jul 29 13:24:15 2013 +0200
1.3 @@ -10,7 +10,6 @@
1.4 type eval
1.5 val eval_eq: eval * eval -> bool
1.6 val eval_result_state: eval -> Toplevel.state
1.7 - val eval_stable: eval -> bool
1.8 val eval: (unit -> theory) -> Token.T list -> eval -> eval
1.9 type print
1.10 val print: bool -> string -> eval -> print list -> print list option
1.11 @@ -28,7 +27,7 @@
1.12 structure Command: COMMAND =
1.13 struct
1.14
1.15 -(** memo results -- including physical interrupts! **)
1.16 +(** memo results -- including physical interrupts **)
1.17
1.18 datatype 'a expr =
1.19 Expr of Document_ID.exec * (unit -> 'a) |
1.20 @@ -45,11 +44,6 @@
1.21 Expr (exec_id, _) => error ("Unfinished execution result: " ^ Document_ID.print exec_id)
1.22 | Result res => Exn.release res);
1.23
1.24 -fun memo_stable (Memo v) =
1.25 - (case Synchronized.value v of
1.26 - Expr _ => true
1.27 - | Result res => not (Exn.is_interrupt_exn res));
1.28 -
1.29 fun memo_finished (Memo v) =
1.30 (case Synchronized.value v of
1.31 Expr _ => false
1.32 @@ -125,9 +119,6 @@
1.33 fun eval_result (Eval {eval_process, ...}) = memo_result eval_process;
1.34 val eval_result_state = #state o eval_result;
1.35
1.36 -fun eval_stable (Eval {exec_id, eval_process}) =
1.37 - Goal.stable_futures exec_id andalso memo_stable eval_process;
1.38 -
1.39 local
1.40
1.41 fun run int tr st =
1.42 @@ -220,11 +211,7 @@
1.43
1.44 fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id';
1.45
1.46 -fun print_stable (Print {exec_id, print_process, ...}) =
1.47 - Goal.stable_futures exec_id andalso memo_stable print_process;
1.48 -
1.49 -fun print_finished (Print {exec_id, print_process, ...}) =
1.50 - Goal.stable_futures exec_id andalso memo_finished print_process;
1.51 +fun print_finished (Print {exec_id, print_process, ...}) = memo_finished print_process;
1.52
1.53 fun print_persistent (Print {persistent, ...}) = persistent;
1.54
1.55 @@ -264,8 +251,8 @@
1.56 if command_visible then
1.57 rev (Synchronized.value print_functions) |> map_filter (fn pr =>
1.58 (case find_first (fn Print {name, ...} => name = fst pr) old_prints of
1.59 - SOME print => if print_stable print then SOME print else new_print pr
1.60 - | NONE => new_print pr))
1.61 + NONE => new_print pr
1.62 + | some => some))
1.63 else filter (fn print => print_finished print andalso print_persistent print) old_prints;
1.64 in
1.65 if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints
2.1 --- a/src/Pure/PIDE/document.ML Mon Jul 29 13:00:36 2013 +0200
2.2 +++ b/src/Pure/PIDE/document.ML Mon Jul 29 13:24:15 2013 +0200
2.3 @@ -41,7 +41,7 @@
2.4 abstype node = Node of
2.5 {header: node_header, (*master directory, theory header, errors*)
2.6 perspective: perspective, (*visible commands, last visible command*)
2.7 - entries: Command.exec option Entries.T * bool, (*command entries with excecutions, stable*)
2.8 + entries: Command.exec option Entries.T, (*command entries with excecutions*)
2.9 result: Command.eval option} (*result of last execution*)
2.10 and version = Version of node String_Graph.T (*development graph wrt. static imports*)
2.11 with
2.12 @@ -58,9 +58,8 @@
2.13 val no_header = ("", Thy_Header.make ("", Position.none) [] [], ["Bad theory header"]);
2.14 val no_perspective = make_perspective [];
2.15
2.16 -val empty_node = make_node (no_header, no_perspective, (Entries.empty, true), NONE);
2.17 -val clear_node =
2.18 - map_node (fn (header, _, _, _) => (header, no_perspective, (Entries.empty, true), NONE));
2.19 +val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE);
2.20 +val clear_node = map_node (fn (header, _, _, _) => (header, no_perspective, Entries.empty, NONE));
2.21
2.22
2.23 (* basic components *)
2.24 @@ -87,17 +86,11 @@
2.25 val visible_node = is_some o visible_last
2.26
2.27 fun map_entries f =
2.28 - map_node (fn (header, perspective, (entries, stable), result) =>
2.29 - (header, perspective, (f entries, stable), result));
2.30 -fun get_entries (Node {entries = (entries, _), ...}) = entries;
2.31 -
2.32 -fun entries_stable stable =
2.33 - map_node (fn (header, perspective, (entries, _), result) =>
2.34 - (header, perspective, (entries, stable), result));
2.35 -fun stable_entries (Node {entries = (_, stable), ...}) = stable;
2.36 + map_node (fn (header, perspective, entries, result) => (header, perspective, f entries, result));
2.37 +fun get_entries (Node {entries, ...}) = entries;
2.38
2.39 fun iterate_entries f = Entries.iterate NONE f o get_entries;
2.40 -fun iterate_entries_after start f (Node {entries = (entries, _), ...}) =
2.41 +fun iterate_entries_after start f (Node {entries, ...}) =
2.42 (case Entries.get_after entries start of
2.43 NONE => I
2.44 | SOME id => Entries.iterate (SOME id) f entries);
2.45 @@ -328,7 +321,6 @@
2.46 type assign_update = Command.exec option Inttab.table; (*command id -> exec*)
2.47
2.48 val assign_update_empty: assign_update = Inttab.empty;
2.49 -fun assign_update_null (tab: assign_update) = Inttab.is_empty tab;
2.50 fun assign_update_defined (tab: assign_update) command_id = Inttab.defined tab command_id;
2.51 fun assign_update_apply (tab: assign_update) node = Inttab.fold assign_entry tab node;
2.52
2.53 @@ -402,8 +394,7 @@
2.54 val flags' = update_flags prev flags;
2.55 val same' =
2.56 (case (lookup_entry node0 command_id, opt_exec) of
2.57 - (SOME (eval0, _), SOME (eval, _)) =>
2.58 - Command.eval_eq (eval0, eval) andalso Command.eval_stable eval
2.59 + (SOME (eval0, _), SOME (eval, _)) => Command.eval_eq (eval0, eval)
2.60 | _ => false);
2.61 val assign_update' = assign_update |> same' ?
2.62 (case opt_exec of
2.63 @@ -471,7 +462,7 @@
2.64 val node_required = is_required name;
2.65 in
2.66 if imports_changed orelse AList.defined (op =) edits name orelse
2.67 - not (stable_entries node) orelse not (finished_theory node)
2.68 + not (finished_theory node)
2.69 then
2.70 let
2.71 val node0 = node_of old_version name;
2.72 @@ -512,7 +503,6 @@
2.73
2.74 val node' = node
2.75 |> assign_update_apply assigned_execs
2.76 - |> entries_stable (assign_update_null updated_execs)
2.77 |> set_result result;
2.78 val assigned_node = SOME (name, node');
2.79 val result_changed = changed_result node0 node';
3.1 --- a/src/Pure/goal.ML Mon Jul 29 13:00:36 2013 +0200
3.2 +++ b/src/Pure/goal.ML Mon Jul 29 13:24:15 2013 +0200
3.3 @@ -27,7 +27,6 @@
3.4 val fork_params: {name: string, pos: Position.T, pri: int} -> (unit -> 'a) -> 'a future
3.5 val fork: int -> (unit -> 'a) -> 'a future
3.6 val peek_futures: int -> unit future list
3.7 - val stable_futures: int-> bool
3.8 val reset_futures: unit -> Future.group list
3.9 val shutdown_futures: unit -> unit
3.10 val skip_proofs_enabled: unit -> bool
3.11 @@ -181,9 +180,6 @@
3.12 fun peek_futures id =
3.13 Inttab.lookup_list (#3 (Synchronized.value forked_proofs)) id;
3.14
3.15 -fun stable_futures id =
3.16 - not (Par_Exn.is_interrupted (map_filter Future.peek (peek_futures id)));
3.17 -
3.18 fun reset_futures () =
3.19 Synchronized.change_result forked_proofs (fn (_, groups, _) =>
3.20 (Future.forked_proofs := 0; (groups, (0, [], Inttab.empty))));