# HG changeset patch # User wenzelm # Date 1313873179 -7200 # Node ID d453faed48158e563987aa68cc5781c91ae7d26b # Parent 59ff5a93eef489c402c155dc88d36852928ac754 clarified get_imports -- should not rely on accidental order within graph; diff -r 59ff5a93eef4 -r d453faed4815 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Sat Aug 20 22:28:53 2011 +0200 +++ b/src/Pure/Thy/thy_info.ML Sat Aug 20 22:46:19 2011 +0200 @@ -113,10 +113,6 @@ val is_finished = is_none o get_deps; val master_directory = master_dir o get_deps; -fun get_parents name = - thy_graph Graph.imm_preds name handle Graph.UNDEF _ => - error (loader_msg "nothing known about theory" [name]); - (* access theory *) @@ -130,6 +126,8 @@ SOME theory => theory | _ => error (loader_msg "undefined theory entry for" [name])); +val get_imports = Thy_Load.imports_of o get_theory; + fun loaded_files name = NAMED_CRITICAL "Thy_Info" (fn () => (case get_deps name of NONE => [] @@ -242,7 +240,7 @@ fun check_deps dir name = (case lookup_deps name of - SOME NONE => (true, NONE, get_parents name) + SOME NONE => (true, NONE, get_imports name) | NONE => let val {master, text, imports, ...} = Thy_Load.check_thy dir name in (false, SOME (make_deps master imports, text), imports) end