equal
deleted
inserted
replaced
263 |
263 |
264 fun load_thy last_timing initiators update_time deps text (name, pos) keywords parents = |
264 fun load_thy last_timing initiators update_time deps text (name, pos) keywords parents = |
265 let |
265 let |
266 val _ = kill_thy name; |
266 val _ = kill_thy name; |
267 val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators); |
267 val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators); |
268 val _ = Output.protocol_message (Markup.loading_theory name) "" handle Fail _ => (); |
268 val _ = Output.try_protocol_message (Markup.loading_theory name) ""; |
269 |
269 |
270 val {master = (thy_path, _), imports} = deps; |
270 val {master = (thy_path, _), imports} = deps; |
271 val dir = Path.dir thy_path; |
271 val dir = Path.dir thy_path; |
272 val header = Thy_Header.make (name, pos) imports keywords; |
272 val header = Thy_Header.make (name, pos) imports keywords; |
273 |
273 |