src/Pure/Thy/thy_info.ML
changeset 44337 d453faed4815
parent 44302 0a1934c5c104
child 45666 d83797ef0d2d
equal deleted inserted replaced
44336:59ff5a93eef4 44337:d453faed4815
   111 val get_deps = #1 o get_thy;
   111 val get_deps = #1 o get_thy;
   112 
   112 
   113 val is_finished = is_none o get_deps;
   113 val is_finished = is_none o get_deps;
   114 val master_directory = master_dir o get_deps;
   114 val master_directory = master_dir o get_deps;
   115 
   115 
   116 fun get_parents name =
       
   117   thy_graph Graph.imm_preds name handle Graph.UNDEF _ =>
       
   118     error (loader_msg "nothing known about theory" [name]);
       
   119 
       
   120 
   116 
   121 (* access theory *)
   117 (* access theory *)
   122 
   118 
   123 fun lookup_theory name =
   119 fun lookup_theory name =
   124   (case lookup_thy name of
   120   (case lookup_thy name of
   127 
   123 
   128 fun get_theory name =
   124 fun get_theory name =
   129   (case lookup_theory name of
   125   (case lookup_theory name of
   130     SOME theory => theory
   126     SOME theory => theory
   131   | _ => error (loader_msg "undefined theory entry for" [name]));
   127   | _ => error (loader_msg "undefined theory entry for" [name]));
       
   128 
       
   129 val get_imports = Thy_Load.imports_of o get_theory;
   132 
   130 
   133 fun loaded_files name = NAMED_CRITICAL "Thy_Info" (fn () =>
   131 fun loaded_files name = NAMED_CRITICAL "Thy_Info" (fn () =>
   134   (case get_deps name of
   132   (case get_deps name of
   135     NONE => []
   133     NONE => []
   136   | SOME {master = (thy_path, _), ...} => thy_path :: Thy_Load.loaded_files (get_theory name)));
   134   | SOME {master = (thy_path, _), ...} => thy_path :: Thy_Load.loaded_files (get_theory name)));
   240     fun commit () = update_thy deps theory;
   238     fun commit () = update_thy deps theory;
   241   in (theory, present, commit) end;
   239   in (theory, present, commit) end;
   242 
   240 
   243 fun check_deps dir name =
   241 fun check_deps dir name =
   244   (case lookup_deps name of
   242   (case lookup_deps name of
   245     SOME NONE => (true, NONE, get_parents name)
   243     SOME NONE => (true, NONE, get_imports name)
   246   | NONE =>
   244   | NONE =>
   247       let val {master, text, imports, ...} = Thy_Load.check_thy dir name
   245       let val {master, text, imports, ...} = Thy_Load.check_thy dir name
   248       in (false, SOME (make_deps master imports, text), imports) end
   246       in (false, SOME (make_deps master imports, text), imports) end
   249   | SOME (SOME {master, ...}) =>
   247   | SOME (SOME {master, ...}) =>
   250       let
   248       let