# HG changeset patch # User wenzelm # Date 1185032440 -7200 # Node ID 8babfcaaf12945fa27ed8fabce38e81ac8b41bca # Parent 739707039b0d1fbad0e9994163a8d76297122bd3 deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy); begin_theory: quiet_update_thys in interactive mode, removed no weak_use_thy in batch mode; misc tuning; diff -r 739707039b0d -r 8babfcaaf129 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Sat Jul 21 17:40:39 2007 +0200 +++ b/src/Pure/Thy/thy_info.ML Sat Jul 21 17:40:40 2007 +0200 @@ -97,13 +97,15 @@ {present: bool, (*theory value present*) outdated: bool, (*entry considered outdated*) master: master option, (*master dependencies for thy + attached ML file*) + parents: string list, (*source specification of parents (partially qualified)*) 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 make_deps present outdated master parents files : deps = + {present = present, outdated = outdated, master = master, parents = parents, files = files}; -fun init_deps master files = SOME (make_deps false true master (map (rpair NONE) files)); +fun init_deps master parents files = + SOME (make_deps false true master parents (map (rpair NONE) files)); fun master_idents (NONE: master option) = [] | master_idents (SOME ((_, thy_id), NONE)) = [thy_id] @@ -231,8 +233,8 @@ fun outdate_thy name = if is_finished name orelse is_outdated name then () - else (change_deps name (Option.map (fn {present, outdated = _, master, files} => - make_deps present true master files)); perform Outdate name); + else (change_deps name (Option.map (fn {present, outdated = _, master, parents, files} => + make_deps present true master parents files)); perform Outdate name); fun check_unfinished name = if is_finished name then (warning (loader_msg "tried to touch finished theory" [name]); NONE) @@ -263,11 +265,12 @@ local -fun provide path name info (deps as SOME {present, outdated, master, files}) = +fun provide path name info (deps as SOME {present, outdated, master, parents, files}) = (if AList.defined (op =) files path then () else warning (loader_msg "undeclared dependency of theory" [name] ^ " on file: " ^ quote (Path.implode path)); - SOME (make_deps present outdated master (AList.update (op =) (path, SOME info) files))) + SOME (make_deps present outdated master parents + (AList.update (op =) (path, SOME info) files))) | provide _ _ _ NONE = NONE; fun run_file path = @@ -319,7 +322,8 @@ if null missing_files then () else warning (loader_msg "unresolved dependencies of theory" [name] ^ " on file(s): " ^ commas_quote missing_files); - change_deps name (fn _ => SOME (make_deps true false (SOME master) files)); + change_deps name + (Option.map (fn {parents, ...} => make_deps true false (SOME master) parents files)); perform Update name end; @@ -340,71 +344,75 @@ fun check_deps ml strict dir name = (case lookup_deps name of - NONE => - 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)) + SOME NONE => (true, NONE, get_parents name) + | NONE => + let val (master, (parents, files)) = ThyLoad.deps_thy dir name ml + in (false, init_deps (SOME master) parents files, parents) end + | SOME (deps as SOME {present, outdated, master, parents, files}) => + if present andalso not strict then (true, deps, parents) else - let val (master', (parents', files')) = ThyLoad.deps_thy dir name ml |>> SOME in + let val master' = SOME (ThyLoad.check_thy dir name ml) in if master_idents master <> master_idents master' - then (false, (init_deps master' files', parents')) + then + let val (parents', files') = #2 (ThyLoad.deps_thy dir name ml) + in (false, init_deps master' parents' files', parents') end else let val checked_files = map (check_ml master') files; val current = not outdated andalso forall (is_some o snd) checked_files; - val deps' = SOME (make_deps present (not current) master' checked_files); - in (current, (deps', parents')) end + val deps' = SOME (make_deps present (not current) master' parents checked_files); + in (current, deps', parents) end end); -fun require_thy really ml time strict keep_strict initiators dir str visited = +fun require_thys really ml time strict keep_strict initiators dir strs visited = + fold_map (require_thy really ml time strict keep_strict initiators dir) strs visited +and 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 dir1 = Path.append dir (Path.dir path); + val dir' = 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) + then (true, visited) else let - val (current, (deps, parents)) = check_deps ml strict dir1 name + val (current, deps, parents) = check_deps ml strict dir' 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)); + required_by "\n" initiators); - val dir2 = Path.append dir (master_dir' deps); - val req_parent = require_thy true true time (strict andalso keep_strict) keep_strict - (name :: initiators) dir2; - val (parent_results, visited') = fold_map req_parent parents (name :: visited); + val (parents_current, visited') = + require_thys true true time (strict andalso keep_strict) keep_strict + (name :: initiators) (Path.append dir (master_dir' deps)) parents (name :: visited); - val all_current = current andalso forall fst parent_results; + val all_current = current andalso forall I parents_current; val thy = if all_current orelse not really then SOME (get_theory name) else NONE; 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 dir1 name; - in ((all_current, name), visited') end + else load_thy really ml (time orelse ! Output.timing) initiators dir' name; + in (all_current, visited') end end; -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 dir arg = + Output.toplevel_errors (fn () => (req [] dir arg []; ())) (); -fun gen_use_thy req = gen_use_thy' req Path.current; - -fun warn_finished f name = (check_unfinished warning name; f name); +fun gen_use_thy req str = + let val name = base_name str in + check_unfinished warning name; + gen_use_thy' req Path.current str; + ML_Context.set_context (SOME (Context.Theory (get_theory name))) + end; in -val weak_use_thy = gen_use_thy' (require_thy true true false false false); -val quiet_update_thy = gen_use_thy' (require_thy true true false true true); +val quiet_update_thys = gen_use_thy' (require_thys true true false true true); +val pretend_use_thy_only = gen_use_thy' (require_thy false false false true false) Path.current; -val use_thy = warn_finished (gen_use_thy (require_thy true true false true false)); -val time_use_thy = warn_finished (gen_use_thy (require_thy true true true true false)); -val update_thy = warn_finished (gen_use_thy (require_thy true true false true true)); -val pretend_use_thy_only = warn_finished (gen_use_thy (require_thy false false false true false)); +val use_thy = gen_use_thy (require_thy true true false true false); +val time_use_thy = gen_use_thy (require_thy true true true true false); +val update_thy = gen_use_thy (require_thy true true false true true); end; @@ -432,20 +440,22 @@ fun begin_theory present name parents uses int = let - val bparents = map base_name parents; + val parent_names = map base_name parents; 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) dir) parents; + val _ = if int then quiet_update_thys dir parents else (); + (* FIXME tmp *) + val _ = ML_Context.set_context (SOME (Context.Theory (get_theory (List.last parent_names)))); val _ = check_uses name uses; - val theory = Theory.begin_theory name (map get_theory bparents); + val theory = Theory.begin_theory name (map get_theory parent_names); val deps = if known_thy name then get_deps name - else (init_deps NONE (map #1 uses)); + else init_deps NONE parents (map #1 uses); 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 dir name bparents uses; + val _ = change_thys (update_node name parent_names (deps, SOME (Theory.copy theory))); + val theory' = theory |> present dir name parent_names uses; val _ = put_theory name (Theory.copy theory'); val ((), theory'') = ML_Context.pass_context (Context.Theory theory') (List.app (load_file false)) uses_now