# HG changeset patch
# User wenzelm
# Date 924797927 -7200
# Node ID 453901eb34124f57630a75643182f0d23a759c52
# Parent  1f1d5e00e0a54bf3c7ddb18292c2550893c97434
improved auto dir handling;

diff -r 1f1d5e00e0a5 -r 453901eb3412 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Thu Apr 22 15:16:59 1999 +0200
+++ b/src/Pure/Thy/thy_info.ML	Thu Apr 22 18:18:47 1999 +0200
@@ -249,16 +249,15 @@
               end)
       end);
 
-fun require_thy ml time strict keep_strict initiators s =
+fun require_thy ml time strict keep_strict initiators prfx 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 dir = Path.append prfx (Path.dir path);
 
     val require_parent =
-      #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 =>
+      #1 o require_thy ml time (strict andalso keep_strict) keep_strict (name :: initiators) dir;
+    val (current, (new_deps, parents)) = current_deps ml strict 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;
@@ -269,11 +268,12 @@
         ((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;
+          load_thy ml time initiators 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;
+fun gen_use_thy f s =
+  let val (_, name) = f Path.current 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 []);
diff -r 1f1d5e00e0a5 -r 453901eb3412 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Thu Apr 22 15:16:59 1999 +0200
+++ b/src/Pure/Thy/thy_load.ML	Thu Apr 22 18:18:47 1999 +0200
@@ -19,10 +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: Path.T option -> string -> bool -> (Path.T * File.info) list
-  val deps_thy: Path.T option -> string -> bool ->
+  val check_thy: Path.T -> string -> bool -> (Path.T * File.info) list
+  val deps_thy: Path.T -> 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
+  val load_thy: Path.T -> string -> bool -> bool -> (Path.T * File.info) list
 end;
 
 (*backdoor sealed later*)
@@ -80,8 +80,8 @@
 
 (* check_thy *)
 
-fun tmp_path None f x = f x
-  | tmp_path (Some path) f x = Library.setmp load_path [path] f x;
+fun tmp_path path f x =
+  if Path.is_current path then f x else Library.setmp load_path [path] f x;
 
 fun check_thy_aux name ml =
   (case check_file (thy_path name) of
@@ -104,7 +104,7 @@
 
 fun process_thy dir f name ml =
   let val master = check_thy dir name ml
-  in (master, f (#1 (hd master))) end;
+  in (master, tmp_path dir f (#1 (hd master))) end;
 
 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);