--- a/src/Pure/PIDE/document.ML Fri Apr 06 14:40:00 2012 +0200
+++ b/src/Pure/PIDE/document.ML Fri Apr 06 23:34:38 2012 +0200
@@ -29,7 +29,7 @@
val cancel_execution: state -> Future.task list
val execute: version_id -> state -> state
val update: version_id -> version_id -> edit list -> state ->
- ((command_id * exec_id option) list * (string * command_id option) list) * state
+ (command_id * exec_id option) list * state
val remove_versions: version_id list -> state -> state
val state: unit -> state
val change_state: (state -> state) -> unit
@@ -70,17 +70,16 @@
header: node_header,
perspective: perspective,
entries: (exec_id * exec) option Entries.T, (*command entries with excecutions*)
- last_exec: command_id option, (*last command with exec state assignment*)
result: exec}
and version = Version of node Graph.T (*development graph wrt. static imports*)
with
-fun make_node (touched, header, perspective, entries, last_exec, result) =
+fun make_node (touched, header, perspective, entries, result) =
Node {touched = touched, header = header, perspective = perspective,
- entries = entries, last_exec = last_exec, result = result};
+ entries = entries, result = result};
-fun map_node f (Node {touched, header, perspective, entries, last_exec, result}) =
- make_node (f (touched, header, perspective, entries, last_exec, result));
+fun map_node f (Node {touched, header, perspective, entries, result}) =
+ make_node (f (touched, header, perspective, entries, result));
fun make_perspective command_ids : perspective =
(Inttab.defined (Inttab.make (map (rpair ()) command_ids)), try List.last command_ids);
@@ -88,35 +87,35 @@
val no_header = Exn.Exn (ERROR "Bad theory header");
val no_perspective = make_perspective [];
-val empty_node = make_node (false, no_header, no_perspective, Entries.empty, NONE, no_exec);
-val clear_node = map_node (fn (_, header, _, _, _, _) =>
- (false, header, no_perspective, Entries.empty, NONE, no_exec));
+val empty_node = make_node (false, no_header, no_perspective, Entries.empty, no_exec);
+val clear_node = map_node (fn (_, header, _, _, _) =>
+ (false, header, no_perspective, Entries.empty, no_exec));
(* basic components *)
fun is_touched (Node {touched, ...}) = touched;
fun set_touched touched =
- map_node (fn (_, header, perspective, entries, last_exec, result) =>
- (touched, header, perspective, entries, last_exec, result));
+ map_node (fn (_, header, perspective, entries, result) =>
+ (touched, header, perspective, entries, result));
fun get_header (Node {header, ...}) = header;
fun set_header header =
- map_node (fn (touched, _, perspective, entries, last_exec, result) =>
- (touched, header, perspective, entries, last_exec, result));
+ map_node (fn (touched, _, perspective, entries, result) =>
+ (touched, header, perspective, entries, result));
fun get_perspective (Node {perspective, ...}) = perspective;
fun set_perspective ids =
- map_node (fn (touched, header, _, entries, last_exec, result) =>
- (touched, header, make_perspective ids, entries, last_exec, result));
+ map_node (fn (touched, header, _, entries, result) =>
+ (touched, header, make_perspective ids, entries, result));
val visible_command = #1 o get_perspective;
val visible_last = #2 o get_perspective;
val visible_node = is_some o visible_last
fun map_entries f =
- map_node (fn (touched, header, perspective, entries, last_exec, result) =>
- (touched, header, perspective, f entries, last_exec, result));
+ map_node (fn (touched, header, perspective, entries, result) =>
+ (touched, header, perspective, f entries, result));
fun get_entries (Node {entries, ...}) = entries;
fun iterate_entries f = Entries.iterate NONE f o get_entries;
@@ -125,15 +124,10 @@
NONE => I
| SOME id => Entries.iterate (SOME id) f entries);
-fun get_last_exec (Node {last_exec, ...}) = last_exec;
-fun set_last_exec last_exec =
- map_node (fn (touched, header, perspective, entries, _, result) =>
- (touched, header, perspective, entries, last_exec, result));
-
fun get_result (Node {result, ...}) = result;
fun set_result result =
- map_node (fn (touched, header, perspective, entries, last_exec, _) =>
- (touched, header, perspective, entries, last_exec, result));
+ map_node (fn (touched, header, perspective, entries, _) =>
+ (touched, header, perspective, entries, result));
fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node;
fun default_node name = Graph.default_node (name, empty_node);
@@ -499,7 +493,6 @@
val node' = node
|> fold reset_entry no_execs
|> fold (fn (id, exec) => update_entry id (SOME exec)) execs
- |> set_last_exec last_exec
|> set_result result
|> set_touched false;
in ((no_execs, execs, [(name, node')]), node') end)
@@ -511,11 +504,10 @@
map (rpair NONE) (maps #1 updated) @
map (fn (command_id, (exec_id, _)) => (command_id, SOME exec_id)) (maps #2 updated);
val updated_nodes = maps #3 updated;
- val last_execs = map (fn (name, node) => (name, get_last_exec node)) updated_nodes;
val state' = state
|> define_version new_id (fold put_node updated_nodes new_version);
- in ((command_execs, last_execs), state') end;
+ in (command_execs, state') end;
end;