# HG changeset patch # User wenzelm # Date 1184946857 -7200 # Node ID f40fba467384a3ffbf741fd4ffa43bf3b76c4931 # Parent 09254a1622e3088b8d3aaafc90660ccf972f0700 simplified ThyLoad interfaces: only one additional directory; require_thy: cumulative appending of directory prefix; tuned; diff -r 09254a1622e3 -r f40fba467384 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Fri Jul 20 17:54:17 2007 +0200 +++ b/src/Pure/Thy/thy_info.ML Fri Jul 20 17:54:17 2007 +0200 @@ -38,8 +38,8 @@ val load_file: bool -> Path.T -> unit val use: string -> unit val pretend_use_thy_only: string -> unit - val begin_theory: (Path.T list -> string -> string list -> - (Path.T * bool) list -> theory -> theory) -> + val begin_theory: (Path.T -> string -> string list -> + (Path.T * bool) list -> theory -> theory) -> string -> string list -> (Path.T * bool) list -> bool -> theory val end_theory: theory -> theory val finish: unit -> unit @@ -94,23 +94,27 @@ type master = (Path.T * File.ident) * (Path.T * File.ident) option; type deps = - {present: bool, - outdated: bool, - master: master option, - files: (Path.T * (Path.T * File.ident) option) list}; + {present: bool, (*theory value present*) + outdated: bool, (*entry considered outdated*) + master: master option, (*master dependencies for thy + attached ML file*) + files: (*auxiliary files: source path, physical path + identifier*) + (Path.T * (Path.T * File.ident) option) list}; + +fun make_deps present outdated master files = + {present = present, outdated = outdated, master = master, files = files}: deps; + +fun init_deps master files = SOME (make_deps false true master (map (rpair NONE) files)); fun master_idents (NONE: master option) = [] | master_idents (SOME ((_, thy_id), NONE)) = [thy_id] | master_idents (SOME ((_, thy_id), SOME (_, ml_id))) = [thy_id, ml_id]; -fun master_path (m: master option) = map (Path.dir o fst o fst) (the_list m); -fun master_path' (d: deps option) = maps (master_path o #master) (the_list d); -fun master_path'' d = maps master_path' (the_list d); +fun master_dir (NONE: master option) = Path.current + | master_dir (SOME ((path, _), _)) = Path.dir path; -fun make_deps present outdated master files = - {present = present, outdated = outdated, master = master, files = files}: deps; +fun master_dir' (d: deps option) = the_default Path.current (Option.map (master_dir o #master) d); +fun master_dir'' d = the_default Path.current (Option.map master_dir' d); -fun init_deps master files = SOME (make_deps false true master (map (rpair NONE) files)); type thy = deps option * theory option; @@ -268,12 +272,12 @@ fun run_file path = (case Option.map (Context.theory_name o Context.the_theory) (ML_Context.get_context ()) of - NONE => (ThyLoad.load_ml [] path; ()) + NONE => (ThyLoad.load_ml Path.current path; ()) | SOME name => (case lookup_deps name of SOME deps => - change_deps name (provide path name (ThyLoad.load_ml (master_path' deps) path)) - | NONE => (ThyLoad.load_ml [] path; ()))); + change_deps name (provide path name (ThyLoad.load_ml (master_dir' deps) path)) + | NONE => (ThyLoad.load_ml Path.current path; ()))); in @@ -298,7 +302,7 @@ fun required_by _ [] = "" | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")"; -fun load_thy really ml time initiators dirs name = +fun load_thy really ml time initiators dir name = let val _ = if really then priority ("Loading theory " ^ quote name ^ required_by " " initiators) @@ -306,8 +310,8 @@ val _ = touch_thy name; val master = - if really then ThyLoad.load_thy dirs name ml time - else #1 (ThyLoad.deps_thy dirs name ml); + if really then ThyLoad.load_thy dir name ml time + else #1 (ThyLoad.deps_thy dir name ml); val files = get_files name; val missing_files = map_filter (fn (path, NONE) => SOME (Path.implode path) | _ => NONE) files; @@ -326,24 +330,24 @@ local -fun check_ml master (path, info) = +fun check_ml master (src_path, info) = let val info' = (case info of NONE => NONE | SOME (_, id) => - (case ThyLoad.check_ml (master_path master) path of NONE => NONE + (case ThyLoad.check_ml (master_dir master) src_path of NONE => NONE | SOME (path', id') => if id <> id' then NONE else SOME (path', id'))) - in (path, info') end; + in (src_path, info') end; -fun check_deps ml strict dirs name = +fun check_deps ml strict dir name = (case lookup_deps name of NONE => - let val (master, (parents, files)) = ThyLoad.deps_thy dirs name ml |>> SOME + let val (master, (parents, files)) = ThyLoad.deps_thy dir name ml |>> SOME in (false, (init_deps master files, parents)) end | SOME NONE => (true, (NONE, get_parents name)) | SOME (deps as SOME {present, outdated, master, files}) => if present andalso not strict then (true, (deps, get_parents name)) else - let val (master', (parents', files')) = ThyLoad.deps_thy dirs name ml |>> SOME in + let val (master', (parents', files')) = ThyLoad.deps_thy dir name ml |>> SOME in if master_idents master <> master_idents master' then (false, (init_deps master' files', parents')) else @@ -354,25 +358,25 @@ in (current, (deps', parents')) end end); -fun require_thy really ml time strict keep_strict initiators dirs str visited = +fun require_thy really ml time strict keep_strict initiators dir str visited = let val path = Path.expand (Path.explode str); val name = Path.implode (Path.base path); - val dirs' = Path.dir path :: dirs; + val dir1 = Path.append dir (Path.dir path); val _ = member (op =) initiators name andalso error (cycle_msg initiators); in if known_thy name andalso is_finished name orelse member (op =) visited name then ((true, name), visited) else let - val (current, (deps, parents)) = check_deps ml strict dirs' name + val (current, (deps, parents)) = check_deps ml strict dir1 name handle ERROR msg => cat_error msg (loader_msg "the error(s) above occurred while examining theory" [name] ^ (if null initiators then "" else required_by "\n" initiators)); - val dirs'' = master_path' deps @ dirs; + val dir2 = Path.append dir (master_dir' deps); val req_parent = require_thy true true time (strict andalso keep_strict) keep_strict - (name :: initiators) dirs''; + (name :: initiators) dir2; val (parent_results, visited') = fold_map req_parent parents (name :: visited); val all_current = current andalso forall fst parent_results; @@ -380,15 +384,15 @@ val _ = change_thys (update_node name (map base_name parents) (deps, thy)); val _ = if all_current then () - else load_thy really ml (time orelse ! Output.timing) initiators dirs' name; + else load_thy really ml (time orelse ! Output.timing) initiators dir1 name; in ((all_current, name), visited') end end; -fun gen_use_thy' req dirs s = Output.toplevel_errors (fn () => - let val ((_, name), _) = req [] dirs s [] +fun gen_use_thy' req dir s = Output.toplevel_errors (fn () => + let val ((_, name), _) = req [] dir s [] in ML_Context.set_context (SOME (Context.Theory (get_theory name))) end) (); -fun gen_use_thy req = gen_use_thy' req []; +fun gen_use_thy req = gen_use_thy' req Path.current; fun warn_finished f name = (check_unfinished warning name; f name); @@ -429,10 +433,9 @@ fun begin_theory present name parents uses int = let val bparents = map base_name parents; - val dirs' = master_path'' (lookup_deps name); - val dirs = dirs' @ [Path.current]; + val dir = master_dir'' (lookup_deps name); val _ = check_unfinished error name; - val _ = List.app ((if int then quiet_update_thy else weak_use_thy) dirs) parents; + val _ = List.app ((if int then quiet_update_thy else weak_use_thy) dir) parents; val _ = check_uses name uses; val theory = Theory.begin_theory name (map get_theory bparents); @@ -442,7 +445,7 @@ val uses_now = map_filter (fn (x, true) => SOME x | _ => NONE) uses; val _ = change_thys (update_node name bparents (deps, SOME (Theory.copy theory))); - val theory' = theory |> present dirs' name bparents uses; + val theory' = theory |> present dir name bparents uses; val _ = put_theory name (Theory.copy theory'); val ((), theory'') = ML_Context.pass_context (Context.Theory theory') (List.app (load_file false)) uses_now