src/Pure/PIDE/document.ML
changeset 62895 54c2abe7e9a4
parent 62826 eb94e570c1a4
child 62932 db12de2367ca
     1.1 --- a/src/Pure/PIDE/document.ML	Wed Apr 06 19:50:27 2016 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Wed Apr 06 23:45:19 2016 +0200
     1.3 @@ -210,9 +210,6 @@
     1.4      NONE => err_undef "command entry" id
     1.5    | SOME (exec, _) => exec);
     1.6  
     1.7 -fun the_default_entry node (SOME id) = (id, the_default Command.no_exec (the_entry node id))
     1.8 -  | the_default_entry _ NONE = (Document_ID.none, Command.no_exec);
     1.9 -
    1.10  fun assign_entry (command_id, exec) node =
    1.11    if is_none (Entries.lookup (get_entries node) command_id) then node
    1.12    else map_entries (Entries.update (command_id, exec)) node;
    1.13 @@ -548,6 +545,15 @@
    1.14      val _ = Position.reports (map #2 parents_reports);
    1.15    in Resources.begin_theory master_dir header parents end;
    1.16  
    1.17 +fun check_ml_root node =
    1.18 +  if #1 (#name (#header (get_header node))) = Thy_Header.ml_rootN then
    1.19 +    let
    1.20 +      val master_dir = master_directory node;
    1.21 +      val header = #header (get_header node);
    1.22 +      val parent = Thy_Info.get_theory Thy_Header.ml_bootstrapN;
    1.23 +    in SOME (Resources.begin_theory master_dir header [parent]) end
    1.24 +  else NONE;
    1.25 +
    1.26  fun check_theory full name node =
    1.27    is_some (loaded_theory name) orelse
    1.28    null (#errors (get_header node)) andalso (not full orelse is_some (get_result node));
    1.29 @@ -599,7 +605,7 @@
    1.30        else (common, flags);
    1.31    in (assign_update', common', flags') end;
    1.32  
    1.33 -fun illegal_init _ = error "Illegal theory header after end of theory";
    1.34 +fun illegal_init _ = error "Illegal theory header";
    1.35  
    1.36  fun new_exec keywords state node proper_init command_id' (assign_update, command_exec, init) =
    1.37    if not proper_init andalso is_none init then NONE
    1.38 @@ -651,6 +657,7 @@
    1.39                timeit ("Document.update " ^ name) (fn () =>
    1.40                  Runtime.exn_trace_system (fn () =>
    1.41                    let
    1.42 +                    val ml_root = check_ml_root node;
    1.43                      val keywords = the_default (Session.get_keywords ()) (get_keywords node);
    1.44                      val imports = map (apsnd Future.join) deps;
    1.45                      val imports_result_changed = exists (#4 o #1 o #2) imports;
    1.46 @@ -663,13 +670,18 @@
    1.47                          val node0 = node_of old_version name;
    1.48                          val init = init_theory imports node;
    1.49                          val proper_init =
    1.50 -                          check_theory false name node andalso
    1.51 -                          forall (fn (name, (_, node)) => check_theory true name node) imports;
    1.52 +                          is_some ml_root orelse
    1.53 +                            check_theory false name node andalso
    1.54 +                            forall (fn (name, (_, node)) => check_theory true name node) imports;
    1.55  
    1.56                          val (print_execs, common, (still_visible, initial)) =
    1.57                            if imports_result_changed then (assign_update_empty, NONE, (true, true))
    1.58                            else last_common keywords state node_required node0 node;
    1.59 -                        val common_command_exec = the_default_entry node common;
    1.60 +
    1.61 +                        val common_command_exec =
    1.62 +                          (case common of
    1.63 +                            SOME id => (id, the_default Command.no_exec (the_entry node id))
    1.64 +                          | NONE => (Document_ID.none, Command.init_exec ml_root));
    1.65  
    1.66                          val (updated_execs, (command_id', (eval', _)), _) =
    1.67                            (print_execs, common_command_exec, if initial then SOME init else NONE)
    1.68 @@ -727,4 +739,3 @@
    1.69  val change_state = Synchronized.change global_state;
    1.70  
    1.71  end;
    1.72 -