equal
deleted
inserted
replaced
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 |