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