src/Pure/Thy/thy_info.ML
changeset 6484 3f098b0ec683
parent 6389 da9c26906f3f
child 6487 453901eb3412
     1.1 --- a/src/Pure/Thy/thy_info.ML	Thu Apr 22 13:16:22 1999 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Thu Apr 22 13:28:11 1999 +0200
     1.3 @@ -172,13 +172,13 @@
     1.4  fun required_by [] = ""
     1.5    | required_by initiators = " (required by " ^ show_path (rev initiators) ^ ")";
     1.6  
     1.7 -fun load_thy ml time initiators name parents =
     1.8 +fun load_thy ml time initiators dir name parents =
     1.9    let
    1.10      val _ = if name mem_string initiators then error (cycle_msg name (rev initiators)) else ();
    1.11      val _ = writeln ("Loading theory " ^ quote name ^ required_by initiators);
    1.12  
    1.13      val _ = seq touch_thy (thy_graph Graph.all_succs [name]);
    1.14 -    val master = ThyLoad.load_thy name ml time;
    1.15 +    val master = ThyLoad.load_thy dir name ml time;
    1.16  
    1.17      val files = get_files name;
    1.18      val missing_files = mapfilter (fn (path, None) => Some (Path.pack path) | _ => None) files;
    1.19 @@ -226,16 +226,16 @@
    1.20  
    1.21  fun init_deps master files = Some (make_deps false false master (map (rpair None) files));
    1.22  
    1.23 -fun load_deps name ml =
    1.24 -  let val (master, (parents, files)) = ThyLoad.deps_thy name ml
    1.25 +fun load_deps dir name ml =
    1.26 +  let val (master, (parents, files)) = ThyLoad.deps_thy dir name ml
    1.27    in (Some (init_deps master files), parents) end;
    1.28  
    1.29  fun file_current (_, None) = false
    1.30    | file_current (path, info) = info = ThyLoad.check_file path;
    1.31  
    1.32 -fun current_deps ml strict name =
    1.33 +fun current_deps ml strict dir name =
    1.34    (case lookup_deps name of
    1.35 -    None => (false, load_deps name ml)
    1.36 +    None => (false, load_deps dir name ml)
    1.37    | Some deps =>
    1.38        let val same_deps = (None, thy_graph Graph.imm_preds name) in
    1.39          (case deps of
    1.40 @@ -243,31 +243,37 @@
    1.41          | Some {present, outdated, master, files} =>
    1.42              if present andalso not strict then (true, same_deps)
    1.43              else
    1.44 -              let val master' = ThyLoad.check_thy name ml in
    1.45 -                if master <> master' then (false, load_deps name ml)
    1.46 +              let val master' = ThyLoad.check_thy dir name ml in
    1.47 +                if master <> master' then (false, load_deps dir name ml)
    1.48                  else (not outdated andalso forall file_current files, same_deps)
    1.49                end)
    1.50        end);
    1.51  
    1.52 -fun require_thy ml time strict keep_strict initiators name =
    1.53 +fun require_thy ml time strict keep_strict initiators s =
    1.54    let
    1.55 +    val path = Path.expand (Path.unpack s);
    1.56 +    val name = Path.pack (Path.base path);
    1.57 +    val dir = Path.dir path;
    1.58 +    val opt_dir = if Path.is_current dir then None else Some dir;
    1.59 +
    1.60      val require_parent =
    1.61 -      require_thy ml time (strict andalso keep_strict) keep_strict (name :: initiators);
    1.62 -    val (current, (new_deps, parents)) = current_deps ml strict name handle ERROR =>
    1.63 +      #1 o require_thy ml time (strict andalso keep_strict) keep_strict (name :: initiators);
    1.64 +    val (current, (new_deps, parents)) = current_deps ml strict opt_dir name handle ERROR =>
    1.65        error (loader_msg "The error(s) above occurred while examining theory" [name] ^
    1.66          (if null initiators then "" else "\n" ^ required_by initiators));
    1.67      val parents_current = map require_parent parents;
    1.68 -  in
    1.69 -    if current andalso forall I parents_current then true
    1.70 -    else
    1.71 -      ((case new_deps of
    1.72 -        Some deps => change_thys (update_node name parents (untouch_deps deps, None))
    1.73 -      | None => ());
    1.74 -        load_thy ml time initiators name parents;
    1.75 -        false)
    1.76 -  end;
    1.77  
    1.78 -fun gen_use_thy f name = (f name; Context.context (get_theory name));
    1.79 +    val result =
    1.80 +      if current andalso forall I parents_current then true
    1.81 +      else
    1.82 +        ((case new_deps of
    1.83 +          Some deps => change_thys (update_node name parents (untouch_deps deps, None))
    1.84 +        | None => ());
    1.85 +          load_thy ml time initiators opt_dir name parents;
    1.86 +          false);
    1.87 +  in (result, name) end;
    1.88 +
    1.89 +fun gen_use_thy f s = let val (_, name) = f s in Context.context (get_theory name) end;
    1.90  
    1.91  val weak_use_thy = gen_use_thy (require_thy true false false false []);
    1.92  val use_thy      = gen_use_thy (require_thy true false true false []);
    1.93 @@ -280,7 +286,7 @@
    1.94  
    1.95  fun begin_theory name parents paths =
    1.96    let
    1.97 -    val _ = seq weak_use_thy parents;
    1.98 +    val _ = (map Path.basic parents; seq weak_use_thy parents);
    1.99      val theory = PureThy.begin_theory name (map get_theory parents);
   1.100      val _ = change_thys (update_node name parents (init_deps [] [], Some theory));
   1.101      val use_paths = mapfilter (fn (x, true) => Some x | _ => None) paths;