# 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'');