equal
deleted
inserted
replaced
23 val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy); |
23 val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy); |
24 val provide = Resources.provide (src_path, digest); |
24 val provide = Resources.provide (src_path, digest); |
25 val source = {delimited = true, text = cat_lines lines, pos = pos}; |
25 val source = {delimited = true, text = cat_lines lines, pos = pos}; |
26 in |
26 in |
27 gthy |
27 gthy |
28 |> ML_Context.exec (fn () => ML_Context.eval_source true source) |
28 |> ML_Context.exec (fn () => ML_Context.eval_source {SML = false, verbose = true} source) |
29 |> Local_Theory.propagate_ml_env |
29 |> Local_Theory.propagate_ml_env |
30 |> Context.mapping provide (Local_Theory.background_theory provide) |
30 |> Context.mapping provide (Local_Theory.background_theory provide) |
31 end))); |
31 end))); |
32 |
32 |
33 end; |
33 end; |