# HG changeset patch # User wenzelm # Date 1314969700 -7200 # Node ID 5938beb84adc6243ddf7c3bc1b9c9163438e09dd # Parent 317e4962dd0f5df3099f1687dd43c55f515e5982 more precise iterate_entries_after if start refers to last entry; do not assign exec states after bad theory init; reject illegal theory header after end of theory; diff -r 317e4962dd0f -r 5938beb84adc src/Pure/PIDE/document.ML --- 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);