src/Pure/PIDE/document.ML
changeset 67215 03d0c958d65a
parent 66379 6392766f3c25
child 67380 8bef51521f21
     1.1 --- a/src/Pure/PIDE/document.ML	Sat Dec 16 15:15:51 2017 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Sat Dec 16 16:46:01 2017 +0100
     1.3 @@ -578,14 +578,18 @@
     1.4      val _ = Position.reports (map #2 parents_reports);
     1.5    in Resources.begin_theory master_dir header parents end;
     1.6  
     1.7 -fun check_ml_root node =
     1.8 -  if member (op =) Thy_Header.ml_roots (#1 (#name (#header (get_header node)))) then
     1.9 -    let
    1.10 -      val master_dir = master_directory node;
    1.11 -      val header = #header (get_header node);
    1.12 -      val parent = Thy_Info.get_theory Thy_Header.ml_bootstrapN;
    1.13 -    in SOME (Resources.begin_theory master_dir header [parent]) end
    1.14 -  else NONE;
    1.15 +fun check_root_theory node =
    1.16 +  let
    1.17 +    val master_dir = master_directory node;
    1.18 +    val header = #header (get_header node);
    1.19 +    val header_name = #1 (#name header);
    1.20 +    val parent =
    1.21 +      if header_name = Sessions.root_name then
    1.22 +        SOME (Thy_Info.get_theory Sessions.theory_name)
    1.23 +      else if member (op =) Thy_Header.ml_roots header_name then
    1.24 +        SOME (Thy_Info.get_theory Thy_Header.ml_bootstrapN)
    1.25 +      else NONE;
    1.26 +  in parent |> Option.map (fn thy => Resources.begin_theory master_dir header [thy]) end;
    1.27  
    1.28  fun check_theory full name node =
    1.29    is_some (Thy_Info.lookup_theory name) orelse
    1.30 @@ -688,7 +692,7 @@
    1.31                timeit ("Document.update " ^ name) (fn () =>
    1.32                  Runtime.exn_trace_system (fn () =>
    1.33                    let
    1.34 -                    val ml_root = check_ml_root node;
    1.35 +                    val root_theory = check_root_theory node;
    1.36                      val keywords = the_default (Session.get_keywords ()) (get_keywords node);
    1.37                      val imports = map (apsnd Future.join) deps;
    1.38                      val imports_result_changed = exists (#4 o #1 o #2) imports;
    1.39 @@ -701,7 +705,7 @@
    1.40                          val node0 = node_of old_version name;
    1.41                          val init = init_theory imports node;
    1.42                          val proper_init =
    1.43 -                          is_some ml_root orelse
    1.44 +                          is_some root_theory orelse
    1.45                              check_theory false name node andalso
    1.46                              forall (fn (name, (_, node)) => check_theory true name node) imports;
    1.47  
    1.48 @@ -712,7 +716,7 @@
    1.49                          val common_command_exec =
    1.50                            (case common of
    1.51                              SOME id => (id, the_default Command.no_exec (the_entry node id))
    1.52 -                          | NONE => (Document_ID.none, Command.init_exec ml_root));
    1.53 +                          | NONE => (Document_ID.none, Command.init_exec root_theory));
    1.54  
    1.55                          val (updated_execs, (command_id', exec'), _) =
    1.56                            (print_execs, common_command_exec, if initial then SOME init else NONE)