src/Pure/PIDE/document.ML
changeset 47388 fe4b245af74c
parent 47347 af937661e4a1
child 47389 e8552cba702d
     1.1 --- a/src/Pure/PIDE/document.ML	Fri Apr 06 14:40:00 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Apr 06 23:34:38 2012 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4    val cancel_execution: state -> Future.task list
     1.5    val execute: version_id -> state -> state
     1.6    val update: version_id -> version_id -> edit list -> state ->
     1.7 -    ((command_id * exec_id option) list * (string * command_id option) list) * state
     1.8 +    (command_id * exec_id option) list * state
     1.9    val remove_versions: version_id list -> state -> state
    1.10    val state: unit -> state
    1.11    val change_state: (state -> state) -> unit
    1.12 @@ -70,17 +70,16 @@
    1.13    header: node_header,
    1.14    perspective: perspective,
    1.15    entries: (exec_id * exec) option Entries.T,  (*command entries with excecutions*)
    1.16 -  last_exec: command_id option,  (*last command with exec state assignment*)
    1.17    result: exec}
    1.18  and version = Version of node Graph.T  (*development graph wrt. static imports*)
    1.19  with
    1.20  
    1.21 -fun make_node (touched, header, perspective, entries, last_exec, result) =
    1.22 +fun make_node (touched, header, perspective, entries, result) =
    1.23    Node {touched = touched, header = header, perspective = perspective,
    1.24 -    entries = entries, last_exec = last_exec, result = result};
    1.25 +    entries = entries, result = result};
    1.26  
    1.27 -fun map_node f (Node {touched, header, perspective, entries, last_exec, result}) =
    1.28 -  make_node (f (touched, header, perspective, entries, last_exec, result));
    1.29 +fun map_node f (Node {touched, header, perspective, entries, result}) =
    1.30 +  make_node (f (touched, header, perspective, entries, result));
    1.31  
    1.32  fun make_perspective command_ids : perspective =
    1.33    (Inttab.defined (Inttab.make (map (rpair ()) command_ids)), try List.last command_ids);
    1.34 @@ -88,35 +87,35 @@
    1.35  val no_header = Exn.Exn (ERROR "Bad theory header");
    1.36  val no_perspective = make_perspective [];
    1.37  
    1.38 -val empty_node = make_node (false, no_header, no_perspective, Entries.empty, NONE, no_exec);
    1.39 -val clear_node = map_node (fn (_, header, _, _, _, _) =>
    1.40 -  (false, header, no_perspective, Entries.empty, NONE, no_exec));
    1.41 +val empty_node = make_node (false, no_header, no_perspective, Entries.empty, no_exec);
    1.42 +val clear_node = map_node (fn (_, header, _, _, _) =>
    1.43 +  (false, header, no_perspective, Entries.empty, no_exec));
    1.44  
    1.45  
    1.46  (* basic components *)
    1.47  
    1.48  fun is_touched (Node {touched, ...}) = touched;
    1.49  fun set_touched touched =
    1.50 -  map_node (fn (_, header, perspective, entries, last_exec, result) =>
    1.51 -    (touched, header, perspective, entries, last_exec, result));
    1.52 +  map_node (fn (_, header, perspective, entries, result) =>
    1.53 +    (touched, header, perspective, entries, result));
    1.54  
    1.55  fun get_header (Node {header, ...}) = header;
    1.56  fun set_header header =
    1.57 -  map_node (fn (touched, _, perspective, entries, last_exec, result) =>
    1.58 -    (touched, header, perspective, entries, last_exec, result));
    1.59 +  map_node (fn (touched, _, perspective, entries, result) =>
    1.60 +    (touched, header, perspective, entries, result));
    1.61  
    1.62  fun get_perspective (Node {perspective, ...}) = perspective;
    1.63  fun set_perspective ids =
    1.64 -  map_node (fn (touched, header, _, entries, last_exec, result) =>
    1.65 -    (touched, header, make_perspective ids, entries, last_exec, result));
    1.66 +  map_node (fn (touched, header, _, entries, result) =>
    1.67 +    (touched, header, make_perspective ids, entries, result));
    1.68  
    1.69  val visible_command = #1 o get_perspective;
    1.70  val visible_last = #2 o get_perspective;
    1.71  val visible_node = is_some o visible_last
    1.72  
    1.73  fun map_entries f =
    1.74 -  map_node (fn (touched, header, perspective, entries, last_exec, result) =>
    1.75 -    (touched, header, perspective, f entries, last_exec, result));
    1.76 +  map_node (fn (touched, header, perspective, entries, result) =>
    1.77 +    (touched, header, perspective, f entries, result));
    1.78  fun get_entries (Node {entries, ...}) = entries;
    1.79  
    1.80  fun iterate_entries f = Entries.iterate NONE f o get_entries;
    1.81 @@ -125,15 +124,10 @@
    1.82      NONE => I
    1.83    | SOME id => Entries.iterate (SOME id) f entries);
    1.84  
    1.85 -fun get_last_exec (Node {last_exec, ...}) = last_exec;
    1.86 -fun set_last_exec last_exec =
    1.87 -  map_node (fn (touched, header, perspective, entries, _, result) =>
    1.88 -    (touched, header, perspective, entries, last_exec, result));
    1.89 -
    1.90  fun get_result (Node {result, ...}) = result;
    1.91  fun set_result result =
    1.92 -  map_node (fn (touched, header, perspective, entries, last_exec, _) =>
    1.93 -    (touched, header, perspective, entries, last_exec, result));
    1.94 +  map_node (fn (touched, header, perspective, entries, _) =>
    1.95 +    (touched, header, perspective, entries, result));
    1.96  
    1.97  fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node;
    1.98  fun default_node name = Graph.default_node (name, empty_node);
    1.99 @@ -499,7 +493,6 @@
   1.100                      val node' = node
   1.101                        |> fold reset_entry no_execs
   1.102                        |> fold (fn (id, exec) => update_entry id (SOME exec)) execs
   1.103 -                      |> set_last_exec last_exec
   1.104                        |> set_result result
   1.105                        |> set_touched false;
   1.106                    in ((no_execs, execs, [(name, node')]), node') end)
   1.107 @@ -511,11 +504,10 @@
   1.108        map (rpair NONE) (maps #1 updated) @
   1.109        map (fn (command_id, (exec_id, _)) => (command_id, SOME exec_id)) (maps #2 updated);
   1.110      val updated_nodes = maps #3 updated;
   1.111 -    val last_execs = map (fn (name, node) => (name, get_last_exec node)) updated_nodes;
   1.112  
   1.113      val state' = state
   1.114        |> define_version new_id (fold put_node updated_nodes new_version);
   1.115 -  in ((command_execs, last_execs), state') end;
   1.116 +  in (command_execs, state') end;
   1.117  
   1.118  end;
   1.119