src/Pure/PIDE/document.ML
changeset 44645 5938beb84adc
parent 44644 317e4962dd0f
child 44660 90bab3febb6c
--- 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);