equal
deleted
inserted
replaced
244 fun load_file time path = |
244 fun load_file time path = |
245 if time then |
245 if time then |
246 let val name = Path.pack path in |
246 let val name = Path.pack path in |
247 timeit (fn () => |
247 timeit (fn () => |
248 (writeln ("\n**** Starting file " ^ quote name ^ " ****"); |
248 (writeln ("\n**** Starting file " ^ quote name ^ " ****"); |
249 setmp Library.timing true run_file path; |
249 run_file path; |
250 writeln ("**** Finished file " ^ quote name ^ " ****\n"))) |
250 writeln ("**** Finished file " ^ quote name ^ " ****\n"))) |
251 end |
251 end |
252 else run_file path; |
252 else run_file path; |
253 |
253 |
254 val use = load_file false o Path.unpack; |
254 val use = load_file false o Path.unpack; |
305 if master <> master' then (false, load_deps ml dir name) |
305 if master <> master' then (false, load_deps ml dir name) |
306 else (not outdated andalso forall file_current files, same_deps) |
306 else (not outdated andalso forall file_current files, same_deps) |
307 end) |
307 end) |
308 end); |
308 end); |
309 |
309 |
310 fun require_thy ml time_arg strict keep_strict initiators prfx (visited, str) = |
310 fun require_thy ml time strict keep_strict initiators prfx (visited, str) = |
311 let |
311 let |
312 val path = Path.expand (Path.unpack str); |
312 val path = Path.expand (Path.unpack str); |
313 val name = Path.pack (Path.base path); |
313 val name = Path.pack (Path.base path); |
314 val time = time_arg orelse ! Library.timing; |
|
315 in |
314 in |
316 if name mem_string initiators then error (cycle_msg name initiators) else (); |
315 if name mem_string initiators then error (cycle_msg name initiators) else (); |
317 if known_thy name andalso is_finished name orelse name mem_string visited then |
316 if known_thy name andalso is_finished name orelse name mem_string visited then |
318 (visited, (true, name)) |
317 (visited, (true, name)) |
319 else |
318 else |
331 if current andalso forall #1 parent_results then true |
330 if current andalso forall #1 parent_results then true |
332 else |
331 else |
333 ((case new_deps of |
332 ((case new_deps of |
334 Some deps => change_thys (update_node name parents (deps, None)) |
333 Some deps => change_thys (update_node name parents (deps, None)) |
335 | None => ()); |
334 | None => ()); |
336 load_thy ml time initiators dir name parents; |
335 load_thy ml (time orelse ! Library.timing) initiators dir name parents; |
337 false); |
336 false); |
338 in (visited', (result, name)) end |
337 in (visited', (result, name)) end |
339 end; |
338 end; |
340 |
339 |
341 fun gen_use_thy req s = |
340 fun gen_use_thy req s = |