# HG changeset patch # User wenzelm # Date 933971547 -7200 # Node ID fcce2387ad6d414cb564eaf47e18411a183f866f # Parent ba6f09cd7769eea653d2db103272b27ec52a730b added pretend_use; simplified ML handling; loaded_files: include thy; perform Remove *before* actual deletion; perform: made bullet proof; diff -r ba6f09cd7769 -r fcce2387ad6d src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Fri Aug 06 22:30:42 1999 +0200 +++ b/src/Pure/Thy/thy_info.ML Fri Aug 06 22:32:27 1999 +0200 @@ -35,6 +35,7 @@ val load_file: bool -> Path.T -> unit val use_path: Path.T -> unit val use: string -> unit + val pretend_use: string -> unit val begin_theory: string -> string list -> (Path.T * bool) list -> theory val end_theory: theory -> theory val finish: unit -> unit @@ -54,7 +55,7 @@ val hooks = ref ([]: (action -> string -> unit) list); in fun add_hook f = hooks := f :: ! hooks; - fun perform action name = seq (fn f => f action name) (! hooks); + fun perform action name = seq (fn f => (try (fn () => f action name) (); ())) (! hooks); end; @@ -90,7 +91,7 @@ type deps = {present: bool, outdated: bool, - master: (Path.T * File.info) list, files: (Path.T * (Path.T * File.info) option) list}; + master: ThyLoad.master option, files: (Path.T * (Path.T * File.info) option) list}; fun make_deps present outdated master files = {present = present, outdated = outdated, master = master, files = files}: deps; @@ -131,7 +132,12 @@ fun is_finished name = is_none (get_deps name); fun get_files name = (case get_deps name of Some {files, ...} => files | _ => []); -val loaded_files = mapfilter #2 o get_files; + +fun loaded_files name = + (case get_deps name of + Some {master = Some master, files, ...} => ThyLoad.get_thy master :: mapfilter #2 files + | Some {files, ...} => mapfilter #2 files + | None => []); fun get_preds name = (thy_graph Graph.imm_preds name) handle Graph.UNDEFINED _ => @@ -181,8 +187,11 @@ (* load_file *) -fun run_file path = +local + +fun may_run_file really path = let + val load = ThyLoad.may_load_file really; fun provide name info (deps as Some {present, outdated, master, files}) = if exists (equal path o #1) files then Some (make_deps present outdated master (overwrite (files, (path, Some info)))) @@ -191,12 +200,16 @@ | provide _ _ None = None; in (case apsome PureThy.get_name (Context.get_context ()) of - None => (ThyLoad.load_file path; ()) + None => (load path; ()) | Some name => - if is_some (lookup_thy name) then change_deps name (provide name (ThyLoad.load_file path)) - else (ThyLoad.load_file path; ())) + if is_some (lookup_thy name) then change_deps name (provide name (load path)) + else (load path; ())) end; +val run_file = may_run_file true; + +in + fun load_file false path = run_file path | load_file true path = let val name = Path.pack path in @@ -209,6 +222,9 @@ val use_path = load_file false; val use = use_path o Path.unpack; val time_use = load_file true o Path.unpack; +val pretend_use = may_run_file false o Path.unpack; + +end; (* load_thy *) @@ -229,8 +245,8 @@ in if null missing_files then () else warning (loader_msg "unresolved dependencies of theory" [name] ^ - "\nfile(s): " ^ commas_quote missing_files); - change_deps name (fn _ => Some (make_deps true false master files)); + "\non file(s): " ^ commas_quote missing_files); + change_deps name (fn _ => Some (make_deps true false (Some master) files)); perform Update name end; @@ -239,16 +255,16 @@ fun init_deps master files = Some (make_deps false true master (map (rpair None) files)); -fun load_deps dir name ml = - let val (master, (parents, files)) = ThyLoad.deps_thy dir name ml - in (Some (init_deps master files), parents) end; +fun load_deps dir name = + let val (master, (parents, files)) = ThyLoad.deps_thy dir name + in (Some (init_deps (Some master) files), parents) end; fun file_current (_, None) = false | file_current (path, info) = info = ThyLoad.check_file path; -fun current_deps ml strict dir name = +fun current_deps strict dir name = (case lookup_deps name of - None => (false, load_deps dir name ml) + None => (false, load_deps dir name) | Some deps => let val same_deps = (None, thy_graph Graph.imm_preds name) in (case deps of @@ -256,8 +272,8 @@ | Some {present, outdated, master, files} => if present andalso not strict then (true, same_deps) else - let val master' = ThyLoad.check_thy dir name ml in - if master <> master' then (false, load_deps dir name ml) + let val master' = Some (ThyLoad.check_thy dir name) in + if master <> master' then (false, load_deps dir name) else (not outdated andalso forall file_current files, same_deps) end) end); @@ -274,7 +290,7 @@ val req_parent = 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 => + val (current, (new_deps, parents)) = current_deps 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 (visited', parent_results) = foldl_map req_parent (name :: visited, parents); @@ -309,8 +325,8 @@ else let val succs = thy_graph Graph.all_succs [name] in writeln (loader_msg "removing" succs); - change_thys (Graph.del_nodes succs); - seq (perform Remove) succs + seq (perform Remove) succs; + change_thys (Graph.del_nodes succs) end; @@ -324,7 +340,7 @@ else (); val _ = (map Path.basic parents; seq weak_use_thy parents); val theory = PureThy.begin_theory name (map get_theory parents); - val _ = change_thys (update_node name parents (init_deps [] [], Some theory)); + val _ = change_thys (update_node name parents (init_deps None [], Some theory)); val use_paths = mapfilter (fn (x, true) => Some x | _ => None) paths; in Context.setmp (Some theory) (seq use_path) use_paths; theory end;