# HG changeset patch
# User berghofe
# Date 1090254086 -7200
# Node ID 9feac0b7f935006673314c818c6ee913a7dedecd
# Parent  4f3102b501979a30bc4a8e3d855f0a4f3ed542aa
Some changes to allow qualified theory import.

diff -r 4f3102b50197 -r 9feac0b7f935 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Mon Jul 19 18:19:42 2004 +0200
+++ b/src/Pure/Thy/thy_info.ML	Mon Jul 19 18:21:26 2004 +0200
@@ -265,7 +265,7 @@
 fun required_by _ [] = ""
   | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
 
-fun load_thy really ml time initiators dir name parents =
+fun load_thy really ml time initiators dir name =
   let
     val _ =
       if really then priority ("Loading theory " ^ quote name ^ required_by " " initiators)
@@ -289,6 +289,8 @@
 
 (* require_thy *)
 
+fun base_of_path s = Path.pack (Path.base (Path.unpack s));
+
 local
 
 fun load_deps ml dir name =
@@ -326,21 +328,24 @@
       let
         val dir = Path.append prfx (Path.dir path);
         val req_parent = require_thy true true time (strict andalso keep_strict) keep_strict
-          (name :: initiators) dir;
+          (name :: initiators);
 
         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 required_by "\n" initiators));
-        val (visited', parent_results) = foldl_map req_parent (name :: visited, parents);
+        val dir' = (case new_deps of
+            None => dir
+          | Some (Some {master = Some m, ...}) => Path.dir (fst (ThyLoad.get_thy m)));
+        val (visited', parent_results) = foldl_map (req_parent dir') (name :: visited, parents);
 
         val thy = if not really then Some (get_theory name) else None;
         val result =
           if current andalso forall #1 parent_results then true
           else
             ((case new_deps of
-              Some deps => change_thys (update_node name parents (deps, thy))
+              Some deps => change_thys (update_node name (map base_of_path parents) (deps, thy))
             | None => ());
-             load_thy really ml (time orelse ! Output.timing) initiators dir name parents;
+             load_thy really ml (time orelse ! Output.timing) initiators dir name;
              false);
       in (visited', (result, name)) end
   end;
@@ -382,17 +387,18 @@
 
 fun begin_theory present upd name parents paths =
   let
+    val bparents = map base_of_path parents;
     val assert_thy = if upd then quiet_update_thy true else weak_use_thy;
     val _ = check_unfinished error name;
-    val _ = (map Path.basic parents; seq assert_thy parents);
-    val theory = PureThy.begin_theory name (map get_theory parents);
+    val _ = seq assert_thy parents;
+    val theory = PureThy.begin_theory name (map get_theory bparents);
     val deps =
       if known_thy name then get_deps name
       else (init_deps None (map #1 paths));   (*records additional ML files only!*)
     val use_paths = mapfilter (fn (x, true) => Some x | _ => None) paths;
 
-    val _ = change_thys (update_node name parents (deps, Some (Theory.copy theory)));
-    val theory' = theory |> present name parents paths;
+    val _ = change_thys (update_node name bparents (deps, Some (Theory.copy theory)));
+    val theory' = theory |> present name bparents paths;
     val _ = put_theory name (Theory.copy theory');
     val ((), theory'') = Context.pass_theory theory' (seq (load_file false)) use_paths;
     val _ = put_theory name (Theory.copy theory'');