clarified get_imports -- should not rely on accidental order within graph;
authorwenzelm
Sat Aug 20 22:46:19 2011 +0200 (2011-08-20)
changeset 44337d453faed4815
parent 44336 59ff5a93eef4
child 44338 700008399ee5
clarified get_imports -- should not rely on accidental order within graph;
src/Pure/Thy/thy_info.ML
     1.1 --- a/src/Pure/Thy/thy_info.ML	Sat Aug 20 22:28:53 2011 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Sat Aug 20 22:46:19 2011 +0200
     1.3 @@ -113,10 +113,6 @@
     1.4  val is_finished = is_none o get_deps;
     1.5  val master_directory = master_dir o get_deps;
     1.6  
     1.7 -fun get_parents name =
     1.8 -  thy_graph Graph.imm_preds name handle Graph.UNDEF _ =>
     1.9 -    error (loader_msg "nothing known about theory" [name]);
    1.10 -
    1.11  
    1.12  (* access theory *)
    1.13  
    1.14 @@ -130,6 +126,8 @@
    1.15      SOME theory => theory
    1.16    | _ => error (loader_msg "undefined theory entry for" [name]));
    1.17  
    1.18 +val get_imports = Thy_Load.imports_of o get_theory;
    1.19 +
    1.20  fun loaded_files name = NAMED_CRITICAL "Thy_Info" (fn () =>
    1.21    (case get_deps name of
    1.22      NONE => []
    1.23 @@ -242,7 +240,7 @@
    1.24  
    1.25  fun check_deps dir name =
    1.26    (case lookup_deps name of
    1.27 -    SOME NONE => (true, NONE, get_parents name)
    1.28 +    SOME NONE => (true, NONE, get_imports name)
    1.29    | NONE =>
    1.30        let val {master, text, imports, ...} = Thy_Load.check_thy dir name
    1.31        in (false, SOME (make_deps master imports, text), imports) end