src/Pure/PIDE/document.ML
changeset 52761 909167fdd367
parent 52716 ecb46f11c366
child 52771 5009911c7403
     1.1 --- a/src/Pure/PIDE/document.ML	Mon Jul 29 13:00:36 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Mon Jul 29 13:24:15 2013 +0200
     1.3 @@ -41,7 +41,7 @@
     1.4  abstype node = Node of
     1.5   {header: node_header,  (*master directory, theory header, errors*)
     1.6    perspective: perspective,  (*visible commands, last visible command*)
     1.7 -  entries: Command.exec option Entries.T * bool,  (*command entries with excecutions, stable*)
     1.8 +  entries: Command.exec option Entries.T,  (*command entries with excecutions*)
     1.9    result: Command.eval option}  (*result of last execution*)
    1.10  and version = Version of node String_Graph.T  (*development graph wrt. static imports*)
    1.11  with
    1.12 @@ -58,9 +58,8 @@
    1.13  val no_header = ("", Thy_Header.make ("", Position.none) [] [], ["Bad theory header"]);
    1.14  val no_perspective = make_perspective [];
    1.15  
    1.16 -val empty_node = make_node (no_header, no_perspective, (Entries.empty, true), NONE);
    1.17 -val clear_node =
    1.18 -  map_node (fn (header, _, _, _) => (header, no_perspective, (Entries.empty, true), NONE));
    1.19 +val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE);
    1.20 +val clear_node = map_node (fn (header, _, _, _) => (header, no_perspective, Entries.empty, NONE));
    1.21  
    1.22  
    1.23  (* basic components *)
    1.24 @@ -87,17 +86,11 @@
    1.25  val visible_node = is_some o visible_last
    1.26  
    1.27  fun map_entries f =
    1.28 -  map_node (fn (header, perspective, (entries, stable), result) =>
    1.29 -    (header, perspective, (f entries, stable), result));
    1.30 -fun get_entries (Node {entries = (entries, _), ...}) = entries;
    1.31 -
    1.32 -fun entries_stable stable =
    1.33 -  map_node (fn (header, perspective, (entries, _), result) =>
    1.34 -    (header, perspective, (entries, stable), result));
    1.35 -fun stable_entries (Node {entries = (_, stable), ...}) = stable;
    1.36 +  map_node (fn (header, perspective, entries, result) => (header, perspective, f entries, result));
    1.37 +fun get_entries (Node {entries, ...}) = entries;
    1.38  
    1.39  fun iterate_entries f = Entries.iterate NONE f o get_entries;
    1.40 -fun iterate_entries_after start f (Node {entries = (entries, _), ...}) =
    1.41 +fun iterate_entries_after start f (Node {entries, ...}) =
    1.42    (case Entries.get_after entries start of
    1.43      NONE => I
    1.44    | SOME id => Entries.iterate (SOME id) f entries);
    1.45 @@ -328,7 +321,6 @@
    1.46  type assign_update = Command.exec option Inttab.table;  (*command id -> exec*)
    1.47  
    1.48  val assign_update_empty: assign_update = Inttab.empty;
    1.49 -fun assign_update_null (tab: assign_update) = Inttab.is_empty tab;
    1.50  fun assign_update_defined (tab: assign_update) command_id = Inttab.defined tab command_id;
    1.51  fun assign_update_apply (tab: assign_update) node = Inttab.fold assign_entry tab node;
    1.52  
    1.53 @@ -402,8 +394,7 @@
    1.54            val flags' = update_flags prev flags;
    1.55            val same' =
    1.56              (case (lookup_entry node0 command_id, opt_exec) of
    1.57 -              (SOME (eval0, _), SOME (eval, _)) =>
    1.58 -                Command.eval_eq (eval0, eval) andalso Command.eval_stable eval
    1.59 +              (SOME (eval0, _), SOME (eval, _)) => Command.eval_eq (eval0, eval)
    1.60              | _ => false);
    1.61            val assign_update' = assign_update |> same' ?
    1.62              (case opt_exec of
    1.63 @@ -471,7 +462,7 @@
    1.64                  val node_required = is_required name;
    1.65                in
    1.66                  if imports_changed orelse AList.defined (op =) edits name orelse
    1.67 -                  not (stable_entries node) orelse not (finished_theory node)
    1.68 +                  not (finished_theory node)
    1.69                  then
    1.70                    let
    1.71                      val node0 = node_of old_version name;
    1.72 @@ -512,7 +503,6 @@
    1.73  
    1.74                      val node' = node
    1.75                        |> assign_update_apply assigned_execs
    1.76 -                      |> entries_stable (assign_update_null updated_execs)
    1.77                        |> set_result result;
    1.78                      val assigned_node = SOME (name, node');
    1.79                      val result_changed = changed_result node0 node';