equal
deleted
inserted
replaced
459 val name = Context.theory_name thy; |
459 val name = Context.theory_name thy; |
460 val parents = Theory.parents_of thy; |
460 val parents = Theory.parents_of thy; |
461 val parent_specs = map (parent_link remote_path path) parents; |
461 val parent_specs = map (parent_link remote_path path) parents; |
462 |
462 |
463 fun prep_file (raw_path, loadit) = |
463 fun prep_file (raw_path, loadit) = |
464 (case ThyLoad.check_ml dir raw_path of |
464 (case Thy_Load.check_ml dir raw_path of |
465 SOME (path, _) => |
465 SOME (path, _) => |
466 let |
466 let |
467 val base = Path.base path; |
467 val base = Path.base path; |
468 val base_html = html_ext base; |
468 val base_html = html_ext base; |
469 val _ = add_file (Path.append html_prefix base_html, |
469 val _ = add_file (Path.append html_prefix base_html, |