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;
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@62862
     9
  val ML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
wenzelm@62862
    10
  val SML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
wenzelm@62862
    11
end;
wenzelm@62862
    12
wenzelm@62862
    13
structure ML_File: ML_FILE =
wenzelm@62862
    14
struct
wenzelm@62862
    15
wenzelm@62862
    16
fun command SML debug files = Toplevel.generic_theory (fn gthy =>
wenzelm@62862
    17
  let
wenzelm@62862
    18
    val [{src_path, lines, digest, pos}: Token.file] = files (Context.theory_of gthy);
wenzelm@62862
    19
    val provide = Resources.provide (src_path, digest);
wenzelm@62862
    20
    val source = Input.source true (cat_lines lines) (pos, pos);
wenzelm@62862
    21
    val flags =
wenzelm@62902
    22
      {SML = SML, exchange = false, redirect = true, verbose = true,
wenzelm@62902
    23
        debug = debug, writeln = writeln, warning = warning};
wenzelm@62862
    24
  in
wenzelm@62862
    25
    gthy
wenzelm@62862
    26
    |> ML_Context.exec (fn () => ML_Context.eval_source flags source)
wenzelm@62862
    27
    |> Local_Theory.propagate_ml_env
wenzelm@62862
    28
    |> Context.mapping provide (Local_Theory.background_theory provide)
wenzelm@62862
    29
  end);
wenzelm@62862
    30
wenzelm@62902
    31
val ML = command false;
wenzelm@62902
    32
val SML = command true;
wenzelm@62862
    33
wenzelm@62862
    34
end;