src/Pure/ML/ml_file.ML
author wenzelm
Fri Mar 01 16:49:41 2019 +0100 (4 months ago ago)
changeset 70032 29a4f633609e
parent 68820 2e4df245754e
permissions -rw-r--r--
clarified signature;
more thorough end_pos;
wenzelm@62862
     1
(*  Title:      Pure/ML/ml_file.ML
wenzelm@62862
     2
    Author:     Makarius
wenzelm@62862
     3
wenzelm@62862
     4
Commands to load ML files.
wenzelm@62862
     5
*)
wenzelm@62862
     6
wenzelm@62862
     7
signature ML_FILE =
wenzelm@62862
     8
sig
wenzelm@68820
     9
  val command: string -> bool option -> (theory -> Token.file list) ->
wenzelm@68816
    10
    Toplevel.transition -> Toplevel.transition
wenzelm@62862
    11
  val ML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
wenzelm@62862
    12
  val SML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
wenzelm@62862
    13
end;
wenzelm@62862
    14
wenzelm@62862
    15
structure ML_File: ML_FILE =
wenzelm@62862
    16
struct
wenzelm@62862
    17
wenzelm@68820
    18
fun command environment debug files = Toplevel.generic_theory (fn gthy =>
wenzelm@62862
    19
  let
wenzelm@70032
    20
    val [file: Token.file] = files (Context.theory_of gthy);
wenzelm@70032
    21
    val provide = Resources.provide_file file;
wenzelm@70032
    22
    val source = Token.file_source file;
wenzelm@67377
    23
wenzelm@67381
    24
    val _ = Thy_Output.check_comments (Context.proof_of gthy) (Input.source_explode source);
wenzelm@67377
    25
wenzelm@68816
    26
    val flags: ML_Compiler.flags =
wenzelm@68820
    27
      {environment = environment, redirect = true, verbose = true,
wenzelm@62902
    28
        debug = debug, writeln = writeln, warning = warning};
wenzelm@62862
    29
  in
wenzelm@62862
    30
    gthy
wenzelm@62862
    31
    |> ML_Context.exec (fn () => ML_Context.eval_source flags source)
wenzelm@62862
    32
    |> Local_Theory.propagate_ml_env
wenzelm@62862
    33
    |> Context.mapping provide (Local_Theory.background_theory provide)
wenzelm@62862
    34
  end);
wenzelm@62862
    35
wenzelm@68820
    36
val ML = command "";
wenzelm@68820
    37
val SML = command ML_Env.SML;
wenzelm@62862
    38
wenzelm@62862
    39
end;