equal
deleted
inserted
replaced
179 |
179 |
180 val no_entries = Symtab.make [(no_id, make_entry NONE (SOME no_id))]; |
180 val no_entries = Symtab.make [(no_id, make_entry NONE (SOME no_id))]; |
181 |
181 |
182 fun begin_document (id: document_id) path = |
182 fun begin_document (id: document_id) path = |
183 let |
183 let |
184 val (dir, name) = Thy_Load.split_thy_path path; |
184 val (dir, name) = Thy_Header.split_thy_path path; |
185 val _ = define_document id (make_document dir name no_entries); |
185 val _ = define_document id (make_document dir name no_entries); |
186 in () end; |
186 in () end; |
187 |
187 |
188 fun end_document (id: document_id) = |
188 fun end_document (id: document_id) = |
189 NAMED_CRITICAL "Isar" (fn () => |
189 NAMED_CRITICAL "Isar" (fn () => |