1(*  Title:      Pure/ML/ml_file.ML
2    Author:     Makarius
3
4Commands to load ML files.
5*)
6
7signature ML_FILE =
8sig
9  val ML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
10  val SML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
11end;
12
13structure ML_File: ML_FILE =
14struct
15
16fun command SML debug files = Toplevel.generic_theory (fn gthy =>
17  let
18    val [{src_path, lines, digest, pos}: Token.file] = files (Context.theory_of gthy);
19    val provide = Resources.provide (src_path, digest);
20    val source = Input.source true (cat_lines lines) (pos, pos);
21
22    val _ = Thy_Output.check_comments (Context.proof_of gthy) (Input.source_explode source);
23
24    val flags =
25      {SML = SML, exchange = false, redirect = true, verbose = true,
26        debug = debug, writeln = writeln, warning = warning};
27  in
28    gthy
29    |> ML_Context.exec (fn () => ML_Context.eval_source flags source)
30    |> Local_Theory.propagate_ml_env
31    |> Context.mapping provide (Local_Theory.background_theory provide)
32  end);
33
34val ML = command false;
35val SML = command true;
36
37end;
38