src/Pure/ML/ml_file.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 62902 3c0f53eae166
child 67377 143665524d8e
permissions -rw-r--r--
more robust sorted_entries;
     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 ML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
    10   val SML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
    11 end;
    12 
    13 structure ML_File: ML_FILE =
    14 struct
    15 
    16 fun 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     val flags =
    22       {SML = SML, exchange = false, redirect = true, verbose = true,
    23         debug = debug, writeln = writeln, warning = warning};
    24   in
    25     gthy
    26     |> ML_Context.exec (fn () => ML_Context.eval_source flags source)
    27     |> Local_Theory.propagate_ml_env
    28     |> Context.mapping provide (Local_Theory.background_theory provide)
    29   end);
    30 
    31 val ML = command false;
    32 val SML = command true;
    33 
    34 end;