equal
deleted
inserted
replaced
310 handle ERROR msg => |
310 handle ERROR msg => |
311 cat_error msg |
311 cat_error msg |
312 ("The error(s) above occurred for theory " ^ quote theory_name ^ |
312 ("The error(s) above occurred for theory " ^ quote theory_name ^ |
313 Position.here require_pos ^ required_by "\n" initiators); |
313 Position.here require_pos ^ required_by "\n" initiators); |
314 |
314 |
315 val parents = map (Thy_Header.import_name o #1) imports; |
315 val qualifier' = Resources.theory_qualifier theory_name; |
|
316 val dir' = Path.append dir (master_dir_deps (Option.map #1 deps)); |
|
317 |
|
318 val parents = map (#theory_name o Resources.import_name qualifier' dir' o #1) imports; |
316 val (parents_current, tasks') = |
319 val (parents_current, tasks') = |
317 require_thys document symbols last_timing (theory_name :: initiators) |
320 require_thys document symbols last_timing (theory_name :: initiators) |
318 (Resources.theory_qualifier theory_name) |
321 qualifier' dir' imports tasks; |
319 (Path.append dir (master_dir_deps (Option.map #1 deps))) imports tasks; |
|
320 |
322 |
321 val all_current = current andalso parents_current; |
323 val all_current = current andalso parents_current; |
322 val task = |
324 val task = |
323 if all_current then Finished (get_theory theory_name) |
325 if all_current then Finished (get_theory theory_name) |
324 else |
326 else |