src/Pure/PIDE/document.ML

   val define_command: command_id -> string -> string -> state -> state
   val discontinue_execution: state -> unit
   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
 end;
 

 abstype node = Node of
  {touched: bool,
   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};
-
-fun map_node f (Node {touched, header, perspective, entries, last_exec, result}) =
-  make_node (f (touched, header, perspective, entries, last_exec, result));
+    entries = entries, result = 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);
 
 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;
 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);
 
-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);
 fun update_node name f = default_node name #> Graph.map_node name f;
 

                       else exec;
 
                     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)
             end
           else Future.value (([], [], []), node))

 
     val command_execs =
       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;
 
 
 (* remove versions *)