--- a/src/Pure/PIDE/document.ML Tue Jul 09 16:32:51 2013 +0200
+++ b/src/Pure/PIDE/document.ML Tue Jul 09 17:58:38 2013 +0200
@@ -108,6 +108,12 @@
fun set_result result =
map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result));
+fun changed_result node node' =
+ (case (get_result node, get_result node') of
+ (SOME eval, SOME eval') => #exec_id eval <> #exec_id eval'
+ | (NONE, NONE) => false
+ | _ => true);
+
fun finished_theory node =
(case Exn.capture (Command.eval_result_state o the) (get_result node) of
Exn.Res st => can (Toplevel.end_theory Position.none) st
@@ -144,11 +150,9 @@
fun the_default_entry node (SOME id) = (id, the_default Command.no_exec (the_entry node id))
| the_default_entry _ NONE = (Document_ID.none, Command.no_exec);
-fun update_entry id exec =
- map_entries (Entries.update (id, exec));
-
-fun reset_entry id node =
- if is_some (lookup_entry node id) then update_entry id NONE node else node;
+fun assign_entry (command_id, exec) node =
+ if is_none (Entries.lookup (get_entries node) command_id) then node
+ else map_entries (Entries.update (command_id, exec)) node;
fun reset_after id entries =
(case Entries.get_after entries id of
@@ -277,6 +281,9 @@
end;
+
+(* remove_versions *)
+
fun remove_versions version_ids state = state |> map_state (fn (versions, _, execution) =>
let
val _ =
@@ -327,6 +334,25 @@
(** document update **)
+(* exec state assignment *)
+
+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;
+
+fun assign_update_new upd (tab: assign_update) =
+ Inttab.update_new upd tab
+ handle Inttab.DUP dup => err_dup "exec state assignment" dup;
+
+fun assign_update_result (tab: assign_update) =
+ Inttab.fold (fn (command_id, exec) => cons (command_id, Command.exec_ids exec)) tab [];
+
+
+(* update *)
+
val timing = Unsynchronized.ref false;
fun timeit msg e = cond_timeit (! timing) msg e;
@@ -405,19 +431,22 @@
fun illegal_init _ = error "Illegal theory header after end of theory";
-fun new_exec state proper_init command_visible command_id' (execs, command_exec, init) =
+fun new_exec state proper_init command_visible command_id' (assign_update, command_exec, init) =
if not proper_init andalso is_none init then NONE
else
let
val (_, (eval, _)) = command_exec;
val (command_name, span) = the_command state command_id' ||> Lazy.force;
- val init' = if Keyword.is_theory_begin command_name then NONE else init;
+
val eval' = Command.eval (fn () => the_default illegal_init init span) span eval;
val prints' = if command_visible then Command.print command_name eval' else [];
- val command_exec' = (command_id', (eval', prints'));
- in SOME (command_exec' :: execs, command_exec', init') end;
+ val exec' = (eval', prints');
-fun update_prints state node command_id =
+ val assign_update' = assign_update_new (command_id', SOME exec') assign_update;
+ val init' = if Keyword.is_theory_begin command_name then NONE else init;
+ in SOME (assign_update', (command_id', (eval', prints')), init') end;
+
+fun update_prints state node command_id assign_update =
(case the_entry node command_id of
SOME (eval, prints) =>
let
@@ -429,10 +458,10 @@
SOME print => if Command.stable_print print then print else new_print
| NONE => new_print));
in
- if eq_list (op = o pairself #exec_id) (prints, prints') then NONE
- else SOME (command_id, (eval, prints'))
+ if eq_list (op = o pairself #exec_id) (prints, prints') then assign_update
+ else assign_update_new (command_id, SOME (eval, prints')) assign_update
end
- | NONE => NONE);
+ | NONE => assign_update);
in
@@ -454,10 +483,10 @@
(fn () =>
let
val imports = map (apsnd Future.join) deps;
- val changed_imports = exists (#4 o #1 o #2) imports;
+ val imports_changed = exists (#3 o #1 o #2) imports;
val node_required = is_required name;
in
- if changed_imports orelse AList.defined (op =) edits name orelse
+ if imports_changed orelse AList.defined (op =) edits name orelse
not (stable_entries node) orelse not (finished_theory node)
then
let
@@ -472,59 +501,54 @@
val last_visible = visible_last node;
val (common, (still_visible, initial)) =
- if changed_imports then (NONE, (true, true))
+ if imports_changed then (NONE, (true, true))
else last_common state last_visible node0 node;
+
val common_command_exec = the_default_entry node common;
val (new_execs, (command_id', (eval', _)), _) =
- ([], common_command_exec, if initial then SOME init else NONE) |>
- (still_visible orelse node_required) ?
+ (assign_update_empty, common_command_exec, if initial then SOME init else NONE)
+ |> (still_visible orelse node_required) ?
iterate_entries_after common
(fn ((prev, id), _) => fn res =>
if not node_required andalso prev = last_visible then NONE
else new_exec state proper_init (visible_command id) id res) node;
val updated_execs =
- (visible_commands, new_execs) |-> Inttab.fold (fn (id, ()) =>
- if exists (fn (_, ({exec_id = id', ...}, _)) => id = id') new_execs then I
- else append (the_list (update_prints state node id)));
+ (visible_commands, new_execs) |-> Inttab.fold (fn (command_id, ()) =>
+ not (assign_update_defined new_execs command_id) ?
+ update_prints state node command_id);
- val no_execs =
- iterate_entries_after common
- (fn ((_, id0), exec0) => fn res =>
+ val assigned_execs =
+ (node0, updated_execs) |-> iterate_entries_after common
+ (fn ((_, command_id0), exec0) => fn res =>
if is_none exec0 then NONE
- else if exists (fn (_, ({exec_id = id, ...}, _)) => id0 = id) updated_execs
- then SOME res
- else SOME (id0 :: res)) node0 [];
+ else if assign_update_defined updated_execs command_id0 then SOME res
+ else SOME (assign_update_new (command_id0, NONE) res));
val last_exec =
if command_id' = Document_ID.none then NONE else SOME command_id';
val result =
- if is_some (after_entry node last_exec) then NONE
+ if is_none last_exec orelse is_some (after_entry node last_exec) then NONE
else SOME eval';
val node' = node
- |> fold reset_entry no_execs
- |> fold (fn (id, exec) => update_entry id (SOME exec)) updated_execs
- |> entries_stable (null updated_execs)
+ |> assign_update_apply assigned_execs
+ |> entries_stable (assign_update_null updated_execs)
|> set_result result;
- val updated_node =
- if null no_execs andalso null updated_execs then NONE
- else SOME (name, node');
- val changed_result = not (null no_execs) orelse not (null new_execs);
- in ((no_execs, updated_execs, updated_node, changed_result), node') end
- else (([], [], NONE, false), node)
+ val assigned_node =
+ if assign_update_null assigned_execs then NONE else SOME (name, node');
+ val result_changed = changed_result node0 node';
+ in
+ ((assign_update_result assigned_execs, assigned_node, result_changed), node')
+ end
+ else (([], NONE, false), node)
end))
|> Future.joins |> map #1);
- val command_execs =
- map (rpair []) (maps #1 updated) @
- map (fn (command_id, exec) => (command_id, Command.exec_ids exec)) (maps #2 updated);
- val updated_nodes = map_filter #3 updated;
-
val state' = state
- |> define_version new_version_id (fold put_node updated_nodes new_version);
- in (command_execs, state') end;
+ |> define_version new_version_id (fold put_node (map_filter #2 updated) new_version);
+ in (maps #1 updated, state') end;
end;