use_thy etc.: may specify path prefix, which is temporarily used as load path;

--- a/src/Pure/Thy/thy_info.ML	Thu Apr 22 13:16:22 1999 +0200
+++ b/src/Pure/Thy/thy_info.ML	Thu Apr 22 13:28:11 1999 +0200
@@ -172,13 +172,13 @@
 fun required_by [] = ""
   | required_by initiators = " (required by " ^ show_path (rev initiators) ^ ")";
 
-fun load_thy ml time initiators name parents =
+fun load_thy ml time initiators dir name parents =
   let
     val _ = if name mem_string initiators then error (cycle_msg name (rev initiators)) else ();
     val _ = writeln ("Loading theory " ^ quote name ^ required_by initiators);
 
     val _ = seq touch_thy (thy_graph Graph.all_succs [name]);
-    val master = ThyLoad.load_thy name ml time;
+    val master = ThyLoad.load_thy dir name ml time;
 
     val files = get_files name;
     val missing_files = mapfilter (fn (path, None) => Some (Path.pack path) | _ => None) files;
@@ -226,16 +226,16 @@
 
 fun init_deps master files = Some (make_deps false false master (map (rpair None) files));
 
-fun load_deps name ml =
-  let val (master, (parents, files)) = ThyLoad.deps_thy name ml
+fun load_deps dir name ml =
+  let val (master, (parents, files)) = ThyLoad.deps_thy dir name ml
   in (Some (init_deps master files), parents) end;
 
 fun file_current (_, None) = false
   | file_current (path, info) = info = ThyLoad.check_file path;
 
-fun current_deps ml strict name =
+fun current_deps ml strict dir name =
   (case lookup_deps name of
-    None => (false, load_deps name ml)
+    None => (false, load_deps dir name ml)
   | Some deps =>
       let val same_deps = (None, thy_graph Graph.imm_preds name) in
         (case deps of
@@ -243,31 +243,37 @@
         | Some {present, outdated, master, files} =>
             if present andalso not strict then (true, same_deps)
             else
-              let val master' = ThyLoad.check_thy name ml in
-                if master <> master' then (false, load_deps name ml)
+              let val master' = ThyLoad.check_thy dir name ml in
+                if master <> master' then (false, load_deps dir name ml)
                 else (not outdated andalso forall file_current files, same_deps)
               end)
       end);
 
-fun require_thy ml time strict keep_strict initiators name =
+fun require_thy ml time strict keep_strict initiators s =
   let
+    val path = Path.expand (Path.unpack s);
+    val name = Path.pack (Path.base path);
+    val dir = Path.dir path;
+    val opt_dir = if Path.is_current dir then None else Some dir;
+
     val require_parent =
-      require_thy ml time (strict andalso keep_strict) keep_strict (name :: initiators);
-    val (current, (new_deps, parents)) = current_deps ml strict name handle ERROR =>
+      #1 o require_thy ml time (strict andalso keep_strict) keep_strict (name :: initiators);
+    val (current, (new_deps, parents)) = current_deps ml strict opt_dir name handle ERROR =>
       error (loader_msg "The error(s) above occurred while examining theory" [name] ^
         (if null initiators then "" else "\n" ^ required_by initiators));
     val parents_current = map require_parent parents;
-  in
-    if current andalso forall I parents_current then true
-    else
-      ((case new_deps of
-        Some deps => change_thys (update_node name parents (untouch_deps deps, None))
-      | None => ());
-        load_thy ml time initiators name parents;
-        false)
-  end;
 
-fun gen_use_thy f name = (f name; Context.context (get_theory name));
+    val result =
+      if current andalso forall I parents_current then true
+      else
+        ((case new_deps of
+          Some deps => change_thys (update_node name parents (untouch_deps deps, None))
+        | None => ());
+          load_thy ml time initiators opt_dir name parents;
+          false);
+  in (result, name) end;
+
+fun gen_use_thy f s = let val (_, name) = f s in Context.context (get_theory name) end;
 
 val weak_use_thy = gen_use_thy (require_thy true false false false []);
 val use_thy      = gen_use_thy (require_thy true false true false []);
@@ -280,7 +286,7 @@
 
 fun begin_theory name parents paths =
   let
-    val _ = seq weak_use_thy parents;
+    val _ = (map Path.basic parents; seq weak_use_thy parents);
     val theory = PureThy.begin_theory name (map get_theory parents);
     val _ = change_thys (update_node name parents (init_deps [] [], Some theory));
     val use_paths = mapfilter (fn (x, true) => Some x | _ => None) paths;

--- a/src/Pure/Thy/thy_load.ML	Thu Apr 22 13:16:22 1999 +0200
+++ b/src/Pure/Thy/thy_load.ML	Thu Apr 22 13:28:11 1999 +0200
@@ -19,9 +19,10 @@
   val ml_path: string -> Path.T
   val check_file: Path.T -> (Path.T * File.info) option
   val load_file: Path.T -> (Path.T * File.info)
-  val check_thy: string -> bool -> (Path.T * File.info) list
-  val deps_thy: string -> bool -> (Path.T * File.info) list * (string list * Path.T list)
-  val load_thy: string -> bool -> bool -> (Path.T * File.info) list
+  val check_thy: Path.T option -> string -> bool -> (Path.T * File.info) list
+  val deps_thy: Path.T option -> string -> bool ->
+    (Path.T * File.info) list * (string list * Path.T list)
+  val load_thy: Path.T option -> string -> bool -> bool -> (Path.T * File.info) list
 end;
 
 (*backdoor sealed later*)
@@ -42,7 +43,7 @@
 fun change_path f = load_path := f (! load_path);
 
 fun show_path () = map Path.pack (! load_path);
-fun add_path s = change_path (fn path => path @ [Path.unpack s]);
+fun add_path s = change_path (cons (Path.unpack s));
 fun del_path s = change_path (filter_out (equal (Path.unpack s)));
 fun reset_path () = load_path := [Path.current];
 
@@ -79,14 +80,20 @@
 
 (* check_thy *)
 
-fun check_thy name ml =
+fun tmp_path None f x = f x
+  | tmp_path (Some path) f x = Library.setmp load_path [path] f x;
+
+fun check_thy_aux name ml =
   (case check_file (thy_path name) of
-    None => error ("Could not find theory file for " ^ quote name)
+    None => error ("Could not find theory file for " ^ quote name ^ " in dir(s) " ^
+      commas_quote (show_path ()))
   | Some thy_info => thy_info ::
       (case if ml then check_file (ml_path name) else None of
         None => []
       | Some info => [info]));
 
+fun check_thy dir name ml = tmp_path dir (check_thy_aux name) ml;
+
 
 (* process theory files *)
 
@@ -95,12 +102,12 @@
 val deps_thy_fn = ref (undefined: string -> bool -> Path.T -> string list * Path.T list);
 val load_thy_fn = ref (undefined: string -> bool -> bool -> Path.T -> unit);
 
-fun process_thy f name ml =
-  let val master = check_thy name ml
+fun process_thy dir f name ml =
+  let val master = check_thy dir name ml
   in (master, f (#1 (hd master))) end;
 
-fun deps_thy name ml = process_thy (! deps_thy_fn name ml) name ml;
-fun load_thy name ml time = #1 (process_thy (! load_thy_fn name ml time) name ml);
+fun deps_thy dir name ml = process_thy dir (! deps_thy_fn name ml) name ml;
+fun load_thy dir name ml time = #1 (process_thy dir (! load_thy_fn name ml time) name ml);
 
 
 end;