equal
deleted
inserted
replaced
383 |
383 |
384 fun begin_theory present upd name parents paths = |
384 fun begin_theory present upd name parents paths = |
385 let |
385 let |
386 val assert_thy = if upd then quiet_update_thy true else weak_use_thy; |
386 val assert_thy = if upd then quiet_update_thy true else weak_use_thy; |
387 val _ = check_unfinished error name; |
387 val _ = check_unfinished error name; |
388 val _ = priority (loader_msg "looking up" [name]); |
|
389 val _ = (map Path.basic parents; seq assert_thy parents); |
388 val _ = (map Path.basic parents; seq assert_thy parents); |
390 val theory = PureThy.begin_theory name (map get_theory parents); |
389 val theory = PureThy.begin_theory name (map get_theory parents); |
391 val deps = |
390 val deps = |
392 if known_thy name then get_deps name |
391 if known_thy name then get_deps name |
393 else (init_deps None (map #1 paths)); (*records additional ML files only!*) |
392 else (init_deps None (map #1 paths)); (*records additional ML files only!*) |