# HG changeset patch # User wenzelm # Date 933105319 -7200 # Node ID 8142ccd139637b2f0233cb2839fe2ecbc0828f4f # Parent 86583034aacf31ad62b47025b0ff7dbbe7616b03 added update_thy_only; added theory loader action hook; added touch_all_thys; touch_thy: all_succs; diff -r 86583034aacf -r 8142ccd13963 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Tue Jul 27 19:02:43 1999 +0200 +++ b/src/Pure/Thy/thy_info.ML Tue Jul 27 21:55:19 1999 +0200 @@ -18,16 +18,20 @@ val remove_thy: string -> unit val time_use_thy: string -> unit val use_thy_only: string -> unit + val update_thy_only: string -> unit end; signature THY_INFO = sig include BASIC_THY_INFO + datatype action = Update | Outdate | Remove + val str_of_action: action -> string + val add_hook: (action -> string -> unit) -> unit val names: unit -> string list val get_theory: string -> theory - val put_theory: theory -> unit val get_preds: string -> string list val loaded_files: string -> (Path.T * File.info) list + val touch_all_thys: unit -> unit val load_file: bool -> Path.T -> unit val use_path: Path.T -> unit val use: string -> unit @@ -41,6 +45,20 @@ struct +(** theory loader actions and hooks **) + +datatype action = Update | Outdate | Remove; +val str_of_action = fn Update => "Update" | Outdate => "Outdate" | Remove => "Remove"; + +local + 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); +end; + + + (** thy database **) (* messages *) @@ -130,8 +148,7 @@ val theory_of_sign = get_theory o Sign.name_of; val theory_of_thm = theory_of_sign o Thm.sign_of_thm; -fun put_theory theory = - change_thy (PureThy.get_name theory) (fn (deps, _) => (deps, Some theory)); +fun put_theory name theory = change_thy name (fn (deps, _) => (deps, Some theory)); @@ -139,51 +156,27 @@ (* maintain 'outdated' flag *) +local + fun is_outdated name = (case lookup_deps name of Some (Some {outdated, ...}) => outdated | _ => false); fun outdate_thy name = - if is_finished name then () - else change_deps name (apsome (fn {present, outdated = _, master, files} => - make_deps present true master files)); + if is_finished name orelse is_outdated name then () + else (change_deps name (apsome (fn {present, outdated = _, master, files} => + make_deps present true master files)); perform Outdate name); + +in fun touch_thy name = - if is_outdated name then () - else if is_finished name then warning (loader_msg "tried to touch finished theory" [name]) - else - (case filter_out is_outdated (thy_graph Graph.all_succs [name]) \ name of - [] => outdate_thy name - | names => - (warning (loader_msg "the following theories become out-of-date:" names); - seq outdate_thy names; outdate_thy name)); - -val untouch_deps = apsome (fn {present, outdated = _, master, files}: deps => - make_deps present false master files); - - -(* load_thy *) + if is_finished name then warning (loader_msg "tried to touch finished theory" [name]) + else seq outdate_thy (thy_graph Graph.all_succs [name]); -fun required_by [] = "" - | required_by initiators = " (required by " ^ show_path (rev initiators) ^ ")"; - -fun load_thy ml time initiators dir name parents = - let - val _ = if name mem_string initiators then error (cycle_msg name (rev initiators)) else (); - val _ = writeln ("Loading theory " ^ quote name ^ required_by initiators); +fun touch_all_thys () = seq outdate_thy (get_names ()); - val _ = seq touch_thy (thy_graph Graph.all_succs [name]); - val master = ThyLoad.load_thy dir name ml time; - - val files = get_files name; - val missing_files = mapfilter (fn (path, None) => Some (Path.pack path) | _ => None) files; - 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)) - end; +end; (* load_file *) @@ -218,9 +211,33 @@ val time_use = load_file true o Path.unpack; +(* load_thy *) + +fun required_by [] = "" + | required_by initiators = " (required by " ^ show_path (rev initiators) ^ ")"; + +fun load_thy ml time initiators dir name parents = + let + val _ = if name mem_string initiators then error (cycle_msg name (rev initiators)) else (); + val _ = writeln ("Loading theory " ^ quote name ^ required_by initiators); + + val _ = touch_thy name; + val master = ThyLoad.load_thy dir name ml time; + + val files = get_files name; + val missing_files = mapfilter (fn (path, None) => Some (Path.pack path) | _ => None) files; + 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)); + perform Update name + end; + + (* require_thy *) -fun init_deps master files = Some (make_deps false false master (map (rpair None) files)); +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 @@ -258,7 +275,7 @@ 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] ^ + 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); @@ -266,10 +283,10 @@ if current andalso forall #1 parent_results then true else ((case new_deps of - Some deps => change_thys (update_node name parents (untouch_deps deps, None)) + Some deps => change_thys (update_node name parents (deps, None)) | None => ()); - load_thy ml time initiators dir name parents; - false); + load_thy ml time initiators dir name parents; + false); in (visited', (result, name)) end end; @@ -277,11 +294,12 @@ let val (_, (_, name)) = req [] 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); -val update_thy = gen_use_thy (require_thy true false true true); -val time_use_thy = gen_use_thy (require_thy true true true false); -val use_thy_only = gen_use_thy (require_thy false false true false); +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); +val time_use_thy = gen_use_thy (require_thy true true true false); +val use_thy_only = gen_use_thy (require_thy false false true false); +val update_thy = gen_use_thy (require_thy true false true true); +val update_thy_only = gen_use_thy (require_thy false false true true); (* remove_thy *) @@ -291,7 +309,8 @@ else let val succs = thy_graph Graph.all_succs [name] in writeln (loader_msg "removing" succs); - change_thys (Graph.del_nodes succs) + change_thys (Graph.del_nodes succs); + seq (perform Remove) succs end; @@ -310,8 +329,10 @@ in Context.setmp (Some theory) (seq use_path) use_paths; theory end; fun end_theory theory = - let val theory' = PureThy.end_theory theory - in put_theory theory'; theory' end; + let + val theory' = PureThy.end_theory theory; + val name = PureThy.get_name theory; + in put_theory name theory'; theory' end; (* finish all theories *) @@ -343,7 +364,7 @@ in if not (null nonfinished) then err "non-finished parent theories" nonfinished else if not (null variants) then err "different versions of parent theories" variants - else change_thys register + else (change_thys register; perform Update name) end;