src/Pure/PIDE/document.ML

 
 
 (** document structure **)
 
 type node_header = (string * Thy_Header.header) Exn.result;
-type perspective = (command_id -> bool) * command_id option; (*visible commands, last*)
+type perspective = (command_id -> bool) * command_id option;
 structure Entries = Linear_Set(type key = command_id val ord = int_ord);
 
 type exec = (Toplevel.state * unit lazy) Command.memo;  (*eval/print process*)
 val no_exec = Command.memo_value (Toplevel.toplevel, Lazy.value ());
 
 abstype node = Node of
  {header: node_header,
-  perspective: perspective,
+  perspective: perspective,  (*visible commands, last*)
   entries: (exec_id * exec) option Entries.T,  (*command entries with excecutions*)
-  result: exec}
+  result: exec option}  (*result of last execution*)
 and version = Version of node Graph.T  (*development graph wrt. static imports*)
 with
 
 fun make_node (header, perspective, entries, result) =
   Node {header = header, perspective = perspective, entries = entries, result = result};

   (Inttab.defined (Inttab.make (map (rpair ()) command_ids)), try List.last command_ids);
 
 val no_header = Exn.Exn (ERROR "Bad theory header");
 val no_perspective = make_perspective [];
 
-val empty_node = make_node (no_header, no_perspective, Entries.empty, no_exec);
-val clear_node = map_node (fn (header, _, _, _) => (header, no_perspective, Entries.empty, no_exec));
+val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE);
+val clear_node = map_node (fn (header, _, _, _) => (header, no_perspective, Entries.empty, NONE));
 
 
 (* basic components *)
 
 fun get_header (Node {header, ...}) = header;

 (* execute *)
 
 local
 
 fun finished_theory node =
-  (case Exn.capture Command.memo_result (get_result node) of
+  (case Exn.capture (Command.memo_result o the) (get_result node) of
     Exn.Res (st, _) => can (Toplevel.end_theory Position.none) st
   | _ => false);
 
 in
 

 
 local
 
 fun stable_finished_theory node =
   is_some (Exn.get_res (Exn.capture (fn () =>
-    fst (Command.memo_result (get_result node))
+    fst (Command.memo_result (the (get_result node)))
     |> Toplevel.end_theory Position.none
     |> Global_Theory.join_proofs) ()));
 
 fun stable_command exec =
   (case Exn.capture Command.memo_result exec of

       (case Url.explode dir of
         Url.File path => path
       | _ => Path.current);
     val parents =
       #imports header |> map (fn import =>
-        (case Thy_Info.lookup_theory import of  (* FIXME more robust!? *)
+        (case Thy_Info.lookup_theory import of
           SOME thy => thy
         | NONE =>
             Toplevel.end_theory (Position.file_only import)
-              (fst (Command.memo_result
-                (get_result (snd (the (AList.lookup (op =) imports import))))))));
+              (fst
+                (Command.memo_result
+                  (the_default no_exec
+                    (get_result (snd (the (AList.lookup (op =) imports import)))))))));
   in Thy_Load.begin_theory master_dir header parents 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 check_theory full name node =
+  is_some (Thy_Info.lookup_theory name) orelse
+  is_some (Exn.get_res (get_header node)) andalso (not full orelse is_some (get_result node));
 
 fun last_common state last_visible node0 node =
   let
     fun update_flags prev (visible, initial) =
       let

       in (last, update_flags last flags) end
   end;
 
 fun illegal_init () = error "Illegal theory header after end of theory";
 
-fun new_exec state bad_init command_id' (execs, command_exec, init) =
-  if bad_init andalso is_none init then NONE
+fun new_exec state proper_init command_id' (execs, command_exec, init) =
+  if not proper_init andalso is_none init then NONE
   else
     let
       val (name, span) = the_command state command_id' ||> Lazy.force;
       val (modify_init, init') =
         if Keyword.is_theory_begin name then

                   required andalso not (stable_finished_theory node)
                 then
                   let
                     val node0 = node_of old_version name;
                     fun init () = init_theory imports node;
-                    val bad_init =
-                      not (check_theory nodes name andalso forall (check_theory nodes o #1) imports);
+                    val proper_init =
+                      check_theory false name node andalso
+                      forall (fn (name, (_, node)) => check_theory true name node) imports;
 
                     val last_visible = visible_last node;
                     val (common, (visible, initial)) =
                       if updated_imports then (NONE, (true, true))
                       else last_common state last_visible node0 node;

                       ([], common_command_exec, if initial then SOME init else NONE) |>
                       (visible orelse required) ?
                         iterate_entries_after common
                           (fn ((prev, id), _) => fn res =>
                             if not required andalso prev = last_visible then NONE
-                            else new_exec state bad_init id res) node;
+                            else new_exec state proper_init id res) node;
 
                     val no_execs =
                       iterate_entries_after common
                         (fn ((_, id0), exec0) => fn res =>
                           if is_none exec0 then NONE
                           else if exists (fn (_, (id, _)) => id0 = id) new_execs then SOME res
                           else SOME (id0 :: res)) node0 [];
 
                     val last_exec = if command_id' = no_id then NONE else SOME command_id';
                     val result =
-                      if is_some (after_entry node last_exec) then no_exec
-                      else exec';
+                      if is_some (after_entry node last_exec) then NONE
+                      else SOME exec';
 
                     val node' = node
                       |> fold reset_entry no_execs
                       |> fold (fn (id, exec) => update_entry id (SOME exec)) new_execs
                       |> set_result result;