76 |
76 |
77 fun map_entries f (Node {header, entries, result}) = make_node (header, f entries, result); |
77 fun map_entries f (Node {header, entries, result}) = make_node (header, f entries, result); |
78 fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries; |
78 fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries; |
79 fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries; |
79 fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries; |
80 |
80 |
81 fun get_theory (Node {result, ...}) = Toplevel.end_theory Position.none (Lazy.get_finished result); |
81 fun get_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.get_finished result); |
82 fun set_result result = map_node (fn (header, entries, _) => (header, entries, result)); |
82 fun set_result result = map_node (fn (header, entries, _) => (header, entries, result)); |
83 |
83 |
84 val empty_exec = Lazy.value Toplevel.toplevel; |
84 val empty_exec = Lazy.value Toplevel.toplevel; |
85 val empty_node = make_node (Exn.Exn (ERROR "Bad theory header"), Entries.empty, empty_exec); |
85 val empty_node = make_node (Exn.Exn (ERROR "Bad theory header"), Entries.empty, empty_exec); |
86 val clear_node = map_node (fn (header, _, _) => (header, Entries.empty, empty_exec)); |
86 val clear_node = map_node (fn (header, _, _) => (header, Entries.empty, empty_exec)); |
345 val files = map (apfst Path.explode) uses; |
345 val files = map (apfst Path.explode) uses; |
346 |
346 |
347 val parents = |
347 val parents = |
348 imports |> map (fn import => |
348 imports |> map (fn import => |
349 (case AList.lookup (op =) deps import of |
349 (case AList.lookup (op =) deps import of |
350 SOME (_, parent_node) => get_theory parent_node |
350 SOME (_, parent_node) => |
|
351 get_theory (Position.file_only (import ^ ".thy")) parent_node |
351 | NONE => Thy_Info.get_theory (Thy_Info.base_name import))); |
352 | NONE => Thy_Info.get_theory (Thy_Info.base_name import))); |
352 in Thy_Load.begin_theory dir thy_name imports files parents end |
353 in Thy_Load.begin_theory dir thy_name imports files parents end |
353 fun get_command id = |
354 fun get_command id = |
354 (id, the_command state id |> Future.map (Toplevel.modify_init init)); |
355 (id, the_command state id |> Future.map (Toplevel.modify_init init)); |
355 |
356 |