# HG changeset patch # User wenzelm # Date 1186607270 -7200 # Node ID b400ec231fdead5685d0de8ef84bccac45aed9ce # Parent 1fa9852643a3bd5969fe9c040bdd07cf530e027f discontinued attached ML files; end_theory: fail on unresolved dependencies; diff -r 1fa9852643a3 -r b400ec231fde src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Wed Aug 08 23:07:48 2007 +0200 +++ b/src/Pure/Thy/thy_info.ML Wed Aug 08 23:07:50 2007 +0200 @@ -88,15 +88,13 @@ (* thy database *) -type master = (Path.T * File.ident) * (Path.T * File.ident) option; - type deps = - {update_time: int, (*symbolic time of update; negative value means outdated*) - master: master option, (*master dependencies for thy + attached ML file*) - text: string list, (*source text for thy*) - 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}; + {update_time: int, (*symbolic time of update; negative value means outdated*) + master: (Path.T * File.ident) option, (*master dependencies for thy file*) + text: string list, (*source text for thy*) + parents: string list, (*source specification of parents (partially qualified)*) + (*auxiliary files: source path, physical path + identifier*) + files: (Path.T * (Path.T * File.ident) option) list}; fun make_deps update_time master text parents files : deps = {update_time = update_time, master = master, text = text, parents = parents, files = files}; @@ -104,12 +102,8 @@ fun init_deps master text parents files = SOME (make_deps ~1 master text parents (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_dir (NONE: master option) = Path.current - | master_dir (SOME ((path, _), _)) = Path.dir path; +fun master_dir NONE = Path.current + | master_dir (SOME (path, _)) = Path.dir path; 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); @@ -164,7 +158,7 @@ (case get_deps name of NONE => [] | SOME {master, files, ...} => - (case master of SOME ((thy_path, _), _) => [thy_path] | NONE => []) @ + (case master of SOME (thy_path, _) => [thy_path] | NONE => []) @ (map_filter (Option.map #1 o #2) files)); fun get_parents name = @@ -227,11 +221,10 @@ let val files = (case get_deps name of SOME {files, ...} => files | NONE => []); val missing_files = map_filter (fn (path, NONE) => SOME (Path.implode path) | _ => NONE) files; - val _ = - if null missing_files then () - else warning (loader_msg "unresolved dependencies of theory" [name] ^ + val _ = null missing_files orelse + error (loader_msg "unresolved dependencies of theory" [name] ^ " on file(s): " ^ commas_quote missing_files); - in files end; + in () end; (* maintain update_time *) @@ -310,20 +303,19 @@ fun required_by _ [] = "" | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")"; -fun load_thy ml time upd_time initiators dir name = +fun load_thy time upd_time initiators dir name = let val _ = priority ("Loading theory " ^ quote name ^ required_by " " initiators); val (pos, text, files) = (case get_deps name of - SOME {master = SOME ((master_path, _), _), text as _ :: _, files, ...} => + SOME {master = SOME (master_path, _), text as _ :: _, files, ...} => (Position.path master_path, text, files) | _ => error (loader_msg "corrupted dependency information" [name])); val _ = touch_thy name; val _ = CRITICAL (fn () => change_deps name (Option.map (fn {master, text, parents, files, ...} => make_deps upd_time master text parents files))); - val _ = ThyLoad.load_thy dir name pos text ml (time orelse ! Output.timing); - val _ = check_files name; + val _ = ThyLoad.load_thy dir name pos text (time orelse ! Output.timing); in CRITICAL (fn () => (change_deps name @@ -349,14 +341,16 @@ (case lookup_deps name of SOME NONE => (true, NONE, get_parents name) | NONE => - let val {master, text, imports = parents, uses = files} = ThyLoad.deps_thy dir name true + let val {master, text, imports = parents, uses = files} = ThyLoad.deps_thy dir name in (false, init_deps (SOME master) text parents files, parents) end | SOME (deps as SOME {update_time, master, text, parents, files}) => - let val master' as SOME ((thy_path, _), _) = SOME (ThyLoad.check_thy dir name true) in - if master_idents master <> master_idents master' - then + let + val (thy_path, thy_id) = ThyLoad.check_thy dir name; + val master' = SOME (thy_path, thy_id); + in + if Option.map #2 master <> SOME thy_id then let val {text = text', imports = parents', uses = files', ...} = - ThyLoad.deps_thy dir name true; + ThyLoad.deps_thy dir name; in (false, init_deps master' text' parents' files', parents') end else let @@ -401,7 +395,7 @@ val upd_time = serial (); val tasks_graph'' = tasks_graph' |> new_deps name parent_names (if all_current then Task.Finished - else Task.Task (fn () => load_thy true time upd_time initiators dir' name)); + else Task.Task (fn () => load_thy time upd_time initiators dir' name)); val tasks_len'' = if all_current then tasks_len' else tasks_len' + 1; in (all_current, (tasks_graph'', tasks_len'')) end) end; @@ -484,13 +478,6 @@ (* begin / end theory *) -fun check_uses name uses = - let val illegal = map (fn ext => Path.ext ext (Path.basic name)) ("" :: ThyLoad.ml_exts) in - (case find_first (member (op =) illegal o Path.base o Path.expand o #1) uses of - NONE => () - | SOME (path, _) => error ("Illegal use of theory ML file: " ^ quote (Path.implode path))) - end; - fun begin_theory name parents uses int = let val parent_names = map base_name parents; @@ -500,7 +487,6 @@ (* FIXME tmp *) val _ = CRITICAL (fn () => 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 parent_names); @@ -521,6 +507,7 @@ fun end_theory theory = let val name = Context.theory_name theory; + val _ = check_files name; val theory' = Theory.end_theory theory; val _ = change_thy name (fn (deps, _) => (deps, SOME theory')); in theory' end; @@ -535,13 +522,12 @@ val _ = map get_theory (get_parents name); val _ = check_unfinished error name; val _ = touch_thy name; - val files = check_files name; - val master = #master (ThyLoad.deps_thy Path.current name false); + val master = #master (ThyLoad.deps_thy Path.current name); val upd_time = serial (); in CRITICAL (fn () => - (change_deps name - (Option.map (fn {parents, ...} => make_deps upd_time (SOME master) [] parents files)); + (change_deps name (Option.map + (fn {parents, files, ...} => make_deps upd_time (SOME master) [] parents files)); perform Update name)) end;