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