# HG changeset patch # User wenzelm # Date 1375097055 -7200 # Node ID 909167fdd367c76702aea09799c5a932fc6f0267 # Parent 8517172b9626278f645f5ec6579877c09b2cd28b discontinued notion of "stable" result -- running execution is never canceled; diff -r 8517172b9626 -r 909167fdd367 src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Mon Jul 29 13:00:36 2013 +0200 +++ b/src/Pure/PIDE/command.ML Mon Jul 29 13:24:15 2013 +0200 @@ -10,7 +10,6 @@ type eval val eval_eq: eval * eval -> bool val eval_result_state: eval -> Toplevel.state - val eval_stable: eval -> bool val eval: (unit -> theory) -> Token.T list -> eval -> eval type print val print: bool -> string -> eval -> print list -> print list option @@ -28,7 +27,7 @@ structure Command: COMMAND = struct -(** memo results -- including physical interrupts! **) +(** memo results -- including physical interrupts **) datatype 'a expr = Expr of Document_ID.exec * (unit -> 'a) | @@ -45,11 +44,6 @@ Expr (exec_id, _) => error ("Unfinished execution result: " ^ Document_ID.print exec_id) | Result res => Exn.release res); -fun memo_stable (Memo v) = - (case Synchronized.value v of - Expr _ => true - | Result res => not (Exn.is_interrupt_exn res)); - fun memo_finished (Memo v) = (case Synchronized.value v of Expr _ => false @@ -125,9 +119,6 @@ fun eval_result (Eval {eval_process, ...}) = memo_result eval_process; val eval_result_state = #state o eval_result; -fun eval_stable (Eval {exec_id, eval_process}) = - Goal.stable_futures exec_id andalso memo_stable eval_process; - local fun run int tr st = @@ -220,11 +211,7 @@ fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id'; -fun print_stable (Print {exec_id, print_process, ...}) = - Goal.stable_futures exec_id andalso memo_stable print_process; - -fun print_finished (Print {exec_id, print_process, ...}) = - Goal.stable_futures exec_id andalso memo_finished print_process; +fun print_finished (Print {exec_id, print_process, ...}) = memo_finished print_process; fun print_persistent (Print {persistent, ...}) = persistent; @@ -264,8 +251,8 @@ if command_visible then rev (Synchronized.value print_functions) |> map_filter (fn pr => (case find_first (fn Print {name, ...} => name = fst pr) old_prints of - SOME print => if print_stable print then SOME print else new_print pr - | NONE => new_print pr)) + NONE => new_print pr + | some => some)) else filter (fn print => print_finished print andalso print_persistent print) old_prints; in if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints diff -r 8517172b9626 -r 909167fdd367 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Mon Jul 29 13:00:36 2013 +0200 +++ b/src/Pure/PIDE/document.ML Mon Jul 29 13:24:15 2013 +0200 @@ -41,7 +41,7 @@ abstype node = Node of {header: node_header, (*master directory, theory header, errors*) perspective: perspective, (*visible commands, last visible command*) - entries: Command.exec option Entries.T * bool, (*command entries with excecutions, stable*) + entries: Command.exec option Entries.T, (*command entries with excecutions*) result: Command.eval option} (*result of last execution*) and version = Version of node String_Graph.T (*development graph wrt. static imports*) with @@ -58,9 +58,8 @@ val no_header = ("", Thy_Header.make ("", Position.none) [] [], ["Bad theory header"]); val no_perspective = make_perspective []; -val empty_node = make_node (no_header, no_perspective, (Entries.empty, true), NONE); -val clear_node = - map_node (fn (header, _, _, _) => (header, no_perspective, (Entries.empty, true), NONE)); +val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE); +val clear_node = map_node (fn (header, _, _, _) => (header, no_perspective, Entries.empty, NONE)); (* basic components *) @@ -87,17 +86,11 @@ val visible_node = is_some o visible_last fun map_entries f = - map_node (fn (header, perspective, (entries, stable), result) => - (header, perspective, (f entries, stable), result)); -fun get_entries (Node {entries = (entries, _), ...}) = entries; - -fun entries_stable stable = - map_node (fn (header, perspective, (entries, _), result) => - (header, perspective, (entries, stable), result)); -fun stable_entries (Node {entries = (_, stable), ...}) = stable; + map_node (fn (header, perspective, entries, result) => (header, perspective, f entries, result)); +fun get_entries (Node {entries, ...}) = entries; fun iterate_entries f = Entries.iterate NONE f o get_entries; -fun iterate_entries_after start f (Node {entries = (entries, _), ...}) = +fun iterate_entries_after start f (Node {entries, ...}) = (case Entries.get_after entries start of NONE => I | SOME id => Entries.iterate (SOME id) f entries); @@ -328,7 +321,6 @@ type assign_update = Command.exec option Inttab.table; (*command id -> exec*) val assign_update_empty: assign_update = Inttab.empty; -fun assign_update_null (tab: assign_update) = Inttab.is_empty tab; fun assign_update_defined (tab: assign_update) command_id = Inttab.defined tab command_id; fun assign_update_apply (tab: assign_update) node = Inttab.fold assign_entry tab node; @@ -402,8 +394,7 @@ val flags' = update_flags prev flags; val same' = (case (lookup_entry node0 command_id, opt_exec) of - (SOME (eval0, _), SOME (eval, _)) => - Command.eval_eq (eval0, eval) andalso Command.eval_stable eval + (SOME (eval0, _), SOME (eval, _)) => Command.eval_eq (eval0, eval) | _ => false); val assign_update' = assign_update |> same' ? (case opt_exec of @@ -471,7 +462,7 @@ val node_required = is_required name; in if imports_changed orelse AList.defined (op =) edits name orelse - not (stable_entries node) orelse not (finished_theory node) + not (finished_theory node) then let val node0 = node_of old_version name; @@ -512,7 +503,6 @@ val node' = node |> assign_update_apply assigned_execs - |> entries_stable (assign_update_null updated_execs) |> set_result result; val assigned_node = SOME (name, node'); val result_changed = changed_result node0 node'; diff -r 8517172b9626 -r 909167fdd367 src/Pure/goal.ML --- a/src/Pure/goal.ML Mon Jul 29 13:00:36 2013 +0200 +++ b/src/Pure/goal.ML Mon Jul 29 13:24:15 2013 +0200 @@ -27,7 +27,6 @@ val fork_params: {name: string, pos: Position.T, pri: int} -> (unit -> 'a) -> 'a future val fork: int -> (unit -> 'a) -> 'a future val peek_futures: int -> unit future list - val stable_futures: int-> bool val reset_futures: unit -> Future.group list val shutdown_futures: unit -> unit val skip_proofs_enabled: unit -> bool @@ -181,9 +180,6 @@ fun peek_futures id = Inttab.lookup_list (#3 (Synchronized.value forked_proofs)) id; -fun stable_futures id = - not (Par_Exn.is_interrupted (map_filter Future.peek (peek_futures id))); - fun reset_futures () = Synchronized.change_result forked_proofs (fn (_, groups, _) => (Future.forked_proofs := 0; (groups, (0, [], Inttab.empty))));