equal
deleted
inserted
replaced
631 |> Option.map (fn thy => (thy, (pos, Theory.get_markup thy)))); |
631 |> Option.map (fn thy => (thy, (pos, Theory.get_markup thy)))); |
632 |
632 |
633 val parents = |
633 val parents = |
634 if null parents_reports then [Theory.get_pure ()] else map #1 parents_reports; |
634 if null parents_reports then [Theory.get_pure ()] else map #1 parents_reports; |
635 val _ = Position.reports (map #2 parents_reports); |
635 val _ = Position.reports (map #2 parents_reports); |
636 in Resources.begin_theory master_dir header parents end; |
636 val thy = Resources.begin_theory master_dir header parents; |
|
637 val _ = Output.status (Markup.markup_only Markup.initialized); |
|
638 in thy end; |
637 |
639 |
638 fun check_root_theory node = |
640 fun check_root_theory node = |
639 let |
641 let |
640 val master_dir = master_directory node; |
642 val master_dir = master_directory node; |
641 val header = #header (get_header node); |
643 val header = #header (get_header node); |