243 |
243 |
244 (* load_thy *) |
244 (* load_thy *) |
245 |
245 |
246 local |
246 local |
247 |
247 |
248 fun try_ml_file dirs name time = |
248 fun try_ml_file dir name time = |
249 let val path = ThyLoad.ml_path name in |
249 let val path = ThyLoad.ml_path name in |
250 if is_none (ThyLoad.check_file dirs path) then () |
250 if is_none (ThyLoad.check_file dir path) then () |
251 else |
251 else |
252 let |
252 let |
253 val _ = legacy_feature ("loading attached ML script " ^ quote (Path.implode path)); |
253 val _ = legacy_feature ("loading attached ML script " ^ quote (Path.implode path)); |
254 val tr = Toplevel.imperative (fn () => ThyInfo.load_file time path); |
254 val tr = Toplevel.imperative (fn () => ThyInfo.load_file time path); |
255 val tr_name = if time then "time_use" else "use"; |
255 val tr_name = if time then "time_use" else "use"; |
256 in Toplevel.excursion [Toplevel.empty |> Toplevel.name tr_name |> tr] end |
256 in Toplevel.excursion [Toplevel.empty |> Toplevel.name tr_name |> tr] end |
257 end; |
257 end; |
258 |
258 |
259 fun run_thy dirs name time = |
259 fun run_thy dir name time = |
260 let |
260 let |
261 val master as ((path, _), _) = ThyLoad.check_thy dirs name false; |
261 val master as ((path, _), _) = ThyLoad.check_thy dir name false; |
262 val text = Source.of_list (Library.untabify (explode (File.read path))); |
262 val text = Source.of_list (Library.untabify (explode (File.read path))); |
263 |
263 |
264 val _ = Present.init_theory name; |
264 val _ = Present.init_theory name; |
265 val _ = Present.verbatim_source name (fn () => Source.exhaust (Symbol.source false text)); |
265 val _ = Present.verbatim_source name (fn () => Source.exhaust (Symbol.source false text)); |
266 val toks = text |
266 val toks = text |
278 |> Present.theory_output name); |
278 |> Present.theory_output name); |
279 val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else (); |
279 val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else (); |
280 |
280 |
281 in master end; |
281 in master end; |
282 |
282 |
283 fun load_thy dirs name ml time = |
283 fun load_thy dir name ml time = |
284 let |
284 let |
285 val master = run_thy dirs name time; |
285 val master = run_thy dir name time; |
286 val _ = ML_Context.set_context (SOME (Context.Theory (ThyInfo.get_theory name))); |
286 val _ = ML_Context.set_context (SOME (Context.Theory (ThyInfo.get_theory name))); |
287 val _ = if ml then try_ml_file dirs name time else (); |
287 val _ = if ml then try_ml_file dir name time else (); |
288 in master end; |
288 in master end; |
289 |
289 |
290 in |
290 in |
291 |
291 |
292 val _ = ThyLoad.load_thy_fn := load_thy; |
292 val _ = ThyLoad.load_thy_fn := load_thy; |