src/Pure/PIDE/document.ML
changeset 47407 8da23ecc70cd
parent 47406 8818f54773cc
child 47415 c486ac962b89
     1.1 --- a/src/Pure/PIDE/document.ML	Mon Apr 09 19:50:04 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Mon Apr 09 20:42:05 2012 +0200
     1.3 @@ -59,7 +59,7 @@
     1.4  (** document structure **)
     1.5  
     1.6  type node_header = (string * Thy_Header.header) Exn.result;
     1.7 -type perspective = (command_id -> bool) * command_id option; (*visible commands, last*)
     1.8 +type perspective = (command_id -> bool) * command_id option;
     1.9  structure Entries = Linear_Set(type key = command_id val ord = int_ord);
    1.10  
    1.11  type exec = (Toplevel.state * unit lazy) Command.memo;  (*eval/print process*)
    1.12 @@ -67,9 +67,9 @@
    1.13  
    1.14  abstype node = Node of
    1.15   {header: node_header,
    1.16 -  perspective: perspective,
    1.17 +  perspective: perspective,  (*visible commands, last*)
    1.18    entries: (exec_id * exec) option Entries.T,  (*command entries with excecutions*)
    1.19 -  result: exec}
    1.20 +  result: exec option}  (*result of last execution*)
    1.21  and version = Version of node Graph.T  (*development graph wrt. static imports*)
    1.22  with
    1.23  
    1.24 @@ -85,8 +85,8 @@
    1.25  val no_header = Exn.Exn (ERROR "Bad theory header");
    1.26  val no_perspective = make_perspective [];
    1.27  
    1.28 -val empty_node = make_node (no_header, no_perspective, Entries.empty, no_exec);
    1.29 -val clear_node = map_node (fn (header, _, _, _) => (header, no_perspective, Entries.empty, no_exec));
    1.30 +val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE);
    1.31 +val clear_node = map_node (fn (header, _, _, _) => (header, no_perspective, Entries.empty, NONE));
    1.32  
    1.33  
    1.34  (* basic components *)
    1.35 @@ -281,7 +281,7 @@
    1.36  local
    1.37  
    1.38  fun finished_theory node =
    1.39 -  (case Exn.capture Command.memo_result (get_result node) of
    1.40 +  (case Exn.capture (Command.memo_result o the) (get_result node) of
    1.41      Exn.Res (st, _) => can (Toplevel.end_theory Position.none) st
    1.42    | _ => false);
    1.43  
    1.44 @@ -330,7 +330,7 @@
    1.45  
    1.46  fun stable_finished_theory node =
    1.47    is_some (Exn.get_res (Exn.capture (fn () =>
    1.48 -    fst (Command.memo_result (get_result node))
    1.49 +    fst (Command.memo_result (the (get_result node)))
    1.50      |> Toplevel.end_theory Position.none
    1.51      |> Global_Theory.join_proofs) ()));
    1.52  
    1.53 @@ -365,17 +365,19 @@
    1.54        | _ => Path.current);
    1.55      val parents =
    1.56        #imports header |> map (fn import =>
    1.57 -        (case Thy_Info.lookup_theory import of  (* FIXME more robust!? *)
    1.58 +        (case Thy_Info.lookup_theory import of
    1.59            SOME thy => thy
    1.60          | NONE =>
    1.61              Toplevel.end_theory (Position.file_only import)
    1.62 -              (fst (Command.memo_result
    1.63 -                (get_result (snd (the (AList.lookup (op =) imports import))))))));
    1.64 +              (fst
    1.65 +                (Command.memo_result
    1.66 +                  (the_default no_exec
    1.67 +                    (get_result (snd (the (AList.lookup (op =) imports import)))))))));
    1.68    in Thy_Load.begin_theory master_dir header parents end;
    1.69  
    1.70 -fun check_theory nodes name =
    1.71 -  is_some (Thy_Info.lookup_theory name) orelse  (* FIXME more robust!? *)
    1.72 -  is_some (Exn.get_res (get_header (get_node nodes name)));
    1.73 +fun check_theory full name node =
    1.74 +  is_some (Thy_Info.lookup_theory name) orelse
    1.75 +  is_some (Exn.get_res (get_header node)) andalso (not full orelse is_some (get_result node));
    1.76  
    1.77  fun last_common state last_visible node0 node =
    1.78    let
    1.79 @@ -410,8 +412,8 @@
    1.80  
    1.81  fun illegal_init () = error "Illegal theory header after end of theory";
    1.82  
    1.83 -fun new_exec state bad_init command_id' (execs, command_exec, init) =
    1.84 -  if bad_init andalso is_none init then NONE
    1.85 +fun new_exec state proper_init command_id' (execs, command_exec, init) =
    1.86 +  if not proper_init andalso is_none init then NONE
    1.87    else
    1.88      let
    1.89        val (name, span) = the_command state command_id' ||> Lazy.force;
    1.90 @@ -463,8 +465,9 @@
    1.91                    let
    1.92                      val node0 = node_of old_version name;
    1.93                      fun init () = init_theory imports node;
    1.94 -                    val bad_init =
    1.95 -                      not (check_theory nodes name andalso forall (check_theory nodes o #1) imports);
    1.96 +                    val proper_init =
    1.97 +                      check_theory false name node andalso
    1.98 +                      forall (fn (name, (_, node)) => check_theory true name node) imports;
    1.99  
   1.100                      val last_visible = visible_last node;
   1.101                      val (common, (visible, initial)) =
   1.102 @@ -478,7 +481,7 @@
   1.103                          iterate_entries_after common
   1.104                            (fn ((prev, id), _) => fn res =>
   1.105                              if not required andalso prev = last_visible then NONE
   1.106 -                            else new_exec state bad_init id res) node;
   1.107 +                            else new_exec state proper_init id res) node;
   1.108  
   1.109                      val no_execs =
   1.110                        iterate_entries_after common
   1.111 @@ -489,8 +492,8 @@
   1.112  
   1.113                      val last_exec = if command_id' = no_id then NONE else SOME command_id';
   1.114                      val result =
   1.115 -                      if is_some (after_entry node last_exec) then no_exec
   1.116 -                      else exec';
   1.117 +                      if is_some (after_entry node last_exec) then NONE
   1.118 +                      else SOME exec';
   1.119  
   1.120                      val node' = node
   1.121                        |> fold reset_entry no_execs