use_thy etc.: may specify path prefix, which is temporarily used as load path;
authorwenzelm
Thu Apr 22 13:28:11 1999 +0200 (1999-04-22)
changeset 64843f098b0ec683
parent 6483 3e5d450c2b31
child 6485 0d334465f29a
use_thy etc.: may specify path prefix, which is temporarily used as load path;
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_load.ML
     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;
     2.1 --- a/src/Pure/Thy/thy_load.ML	Thu Apr 22 13:16:22 1999 +0200
     2.2 +++ b/src/Pure/Thy/thy_load.ML	Thu Apr 22 13:28:11 1999 +0200
     2.3 @@ -19,9 +19,10 @@
     2.4    val ml_path: string -> Path.T
     2.5    val check_file: Path.T -> (Path.T * File.info) option
     2.6    val load_file: Path.T -> (Path.T * File.info)
     2.7 -  val check_thy: string -> bool -> (Path.T * File.info) list
     2.8 -  val deps_thy: string -> bool -> (Path.T * File.info) list * (string list * Path.T list)
     2.9 -  val load_thy: string -> bool -> bool -> (Path.T * File.info) list
    2.10 +  val check_thy: Path.T option -> string -> bool -> (Path.T * File.info) list
    2.11 +  val deps_thy: Path.T option -> string -> bool ->
    2.12 +    (Path.T * File.info) list * (string list * Path.T list)
    2.13 +  val load_thy: Path.T option -> string -> bool -> bool -> (Path.T * File.info) list
    2.14  end;
    2.15  
    2.16  (*backdoor sealed later*)
    2.17 @@ -42,7 +43,7 @@
    2.18  fun change_path f = load_path := f (! load_path);
    2.19  
    2.20  fun show_path () = map Path.pack (! load_path);
    2.21 -fun add_path s = change_path (fn path => path @ [Path.unpack s]);
    2.22 +fun add_path s = change_path (cons (Path.unpack s));
    2.23  fun del_path s = change_path (filter_out (equal (Path.unpack s)));
    2.24  fun reset_path () = load_path := [Path.current];
    2.25  
    2.26 @@ -79,14 +80,20 @@
    2.27  
    2.28  (* check_thy *)
    2.29  
    2.30 -fun check_thy name ml =
    2.31 +fun tmp_path None f x = f x
    2.32 +  | tmp_path (Some path) f x = Library.setmp load_path [path] f x;
    2.33 +
    2.34 +fun check_thy_aux name ml =
    2.35    (case check_file (thy_path name) of
    2.36 -    None => error ("Could not find theory file for " ^ quote name)
    2.37 +    None => error ("Could not find theory file for " ^ quote name ^ " in dir(s) " ^
    2.38 +      commas_quote (show_path ()))
    2.39    | Some thy_info => thy_info ::
    2.40        (case if ml then check_file (ml_path name) else None of
    2.41          None => []
    2.42        | Some info => [info]));
    2.43  
    2.44 +fun check_thy dir name ml = tmp_path dir (check_thy_aux name) ml;
    2.45 +
    2.46  
    2.47  (* process theory files *)
    2.48  
    2.49 @@ -95,12 +102,12 @@
    2.50  val deps_thy_fn = ref (undefined: string -> bool -> Path.T -> string list * Path.T list);
    2.51  val load_thy_fn = ref (undefined: string -> bool -> bool -> Path.T -> unit);
    2.52  
    2.53 -fun process_thy f name ml =
    2.54 -  let val master = check_thy name ml
    2.55 +fun process_thy dir f name ml =
    2.56 +  let val master = check_thy dir name ml
    2.57    in (master, f (#1 (hd master))) end;
    2.58  
    2.59 -fun deps_thy name ml = process_thy (! deps_thy_fn name ml) name ml;
    2.60 -fun load_thy name ml time = #1 (process_thy (! load_thy_fn name ml time) name ml);
    2.61 +fun deps_thy dir name ml = process_thy dir (! deps_thy_fn name ml) name ml;
    2.62 +fun load_thy dir name ml time = #1 (process_thy dir (! load_thy_fn name ml time) name ml);
    2.63  
    2.64  
    2.65  end;