src/Pure/pure_syn.ML
changeset 56618 874bdedb2313
parent 56304 40274e4f5ebf
child 56895 f058120aaad4
equal deleted inserted replaced
56617:c00646996701 56618:874bdedb2313
    21     (Resources.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy =>
    21     (Resources.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy =>
    22         let
    22         let
    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           val flags = {SML = false, redirect = true, verbose = true};
    26           val flags = {SML = false, exchange = false, redirect = true, verbose = true};
    27         in
    27         in
    28           gthy
    28           gthy
    29           |> ML_Context.exec (fn () => ML_Context.eval_source flags source)
    29           |> ML_Context.exec (fn () => ML_Context.eval_source flags source)
    30           |> Local_Theory.propagate_ml_env
    30           |> Local_Theory.propagate_ml_env
    31           |> Context.mapping provide (Local_Theory.background_theory provide)
    31           |> Context.mapping provide (Local_Theory.background_theory provide)