--- a/src/Pure/PIDE/document.ML Fri Sep 02 11:52:13 2011 +0200
+++ b/src/Pure/PIDE/document.ML Fri Sep 02 15:21:40 2011 +0200
@@ -113,7 +113,12 @@
map_node (fn (touched, header, perspective, entries, last_exec, result) =>
(touched, header, perspective, f entries, last_exec, result));
fun get_entries (Node {entries, ...}) = entries;
-fun iterate_entries start f = Entries.iterate start f o get_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 =
@@ -347,9 +352,7 @@
val _ = Multithreading.interrupted ();
val _ = Toplevel.status tr Markup.forked;
val start = Timing.start ();
- val (errs, result) =
- if Toplevel.is_toplevel st andalso not is_init then ([], SOME st)
- else run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
+ val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
val _ = timing tr (Timing.result start);
val _ = Toplevel.status tr Markup.joined;
val _ = List.app (Toplevel.error_msg tr) errs;
@@ -386,31 +389,51 @@
local
-fun last_common last_visible node0 node =
+fun last_common state last_visible node0 node =
let
- fun get_common ((prev, id), exec) (found, (_, visible)) =
+ fun update_flags prev (visible, initial) =
+ let
+ val visible' = visible andalso prev <> last_visible;
+ val initial' = initial andalso
+ (case prev of
+ NONE => true
+ | SOME id => not (Keyword.is_theory_begin (#1 (the_command state id))));
+ in (visible', initial') end;
+ fun get_common ((prev, id), exec) (found, (_, flags)) =
if found then NONE
else
let val found' = is_none exec orelse exec <> lookup_entry node0 id
- in SOME (found', (prev, visible andalso prev <> last_visible)) end;
- val (found, (common, visible)) = iterate_entries NONE get_common node (false, (NONE, true));
- val common' = if found then common else Entries.get_after (get_entries node) common;
- val visible' = visible andalso common' <> last_visible;
- in (common', visible') end;
+ in SOME (found', (prev, update_flags prev flags)) end;
+ val (found, (common, flags)) =
+ iterate_entries get_common node (false, (NONE, (true, true)));
+ in
+ if found then (common, flags)
+ else
+ let val last = Entries.get_after (get_entries node) common
+ in (last, update_flags last flags) end
+ end;
+
+fun illegal_init () = error "Illegal theory header after end of theory";
-fun new_exec state init command_id' (execs, exec) =
- let
- val (_, tr0) = the_command state command_id';
- val exec_id' = new_id ();
- val exec' =
- snd exec |> Lazy.map (fn (st, _) =>
- let val tr =
- Future.join tr0
- |> Toplevel.modify_init init
- |> Toplevel.put_id (print_id exec_id');
- in run_command tr st end)
- |> pair command_id';
- in ((exec_id', exec') :: execs, exec') end;
+fun new_exec state bad_init command_id' (execs, exec, init) =
+ if bad_init andalso is_none init then NONE
+ else
+ let
+ val (name, tr0) = the_command state command_id';
+ val (modify_init, init') =
+ if Keyword.is_theory_begin name then
+ (Toplevel.modify_init (the_default illegal_init init), NONE)
+ else (I, init);
+ val exec_id' = new_id ();
+ val exec' =
+ snd exec |> Lazy.map (fn (st, _) =>
+ let val tr =
+ Future.join tr0
+ |> modify_init
+ |> Toplevel.put_id (print_id exec_id');
+ in run_command tr st end)
+ |> pair command_id';
+ in SOME ((exec_id', exec') :: execs, exec', init') end;
fun make_required nodes =
let
@@ -422,6 +445,10 @@
all_visible Symtab.empty;
in Symtab.defined required end;
+fun check_theory nodes name =
+ is_some (Thy_Info.lookup_theory name) orelse (* FIXME more robust!? *)
+ is_some (Exn.get_res (get_header (get_node nodes name)));
+
fun init_theory deps name node =
let
val (thy_name, imports, uses) = Exn.release (get_header node);
@@ -459,6 +486,8 @@
let
val node0 = node_of old_version name;
fun init () = init_theory deps name node;
+ val bad_init =
+ not (check_theory nodes name andalso forall (check_theory nodes o #1) deps);
in
(singleton o Future.forks)
{name = "Document.update", group = NONE,
@@ -467,18 +496,19 @@
let
val required = is_required name;
val last_visible = #2 (get_perspective node);
- val (common, visible) = last_common last_visible node0 node;
+ val (common, (visible, initial)) = last_common state last_visible node0 node;
val common_exec = the_exec state (the_default_entry node common);
- val (execs, exec) = ([], common_exec) |>
+ val (execs, exec, _) =
+ ([], common_exec, if initial then SOME init else NONE) |>
(visible orelse required) ?
- iterate_entries (after_entry node common)
+ iterate_entries_after common
(fn ((prev, id), _) => fn res =>
if not required andalso prev = last_visible then NONE
- else SOME (new_exec state init id res)) node;
+ else new_exec state bad_init id res) node;
val no_execs =
- iterate_entries (after_entry node0 common)
+ iterate_entries_after common
(fn ((_, id0), exec0) => fn res =>
if is_none exec0 then NONE
else if exists (fn (_, (id, _)) => id0 = id) execs then SOME res
@@ -538,7 +568,7 @@
(singleton o Future.forks)
{name = "theory:" ^ name, group = SOME (Future.new_group (SOME execution)),
deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false}
- (iterate_entries NONE (fn (_, exec) => fn () => SOME (force_exec node exec)) node));
+ (iterate_entries (fn (_, exec) => fn () => SOME (force_exec node exec)) node));
in (versions, commands, execs, execution) end);