src/Pure/ML/ml_compiler2.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 62944 3ee643c5ed00
permissions -rw-r--r--
more robust sorted_entries;
wenzelm@62817
     1
(*  Title:      Pure/ML/ml_compiler2.ML
wenzelm@62817
     2
    Author:     Makarius
wenzelm@62817
     3
wenzelm@62902
     4
Isabelle/ML file operations.
wenzelm@62817
     5
*)
wenzelm@62817
     6
wenzelm@62902
     7
val {ML_file, ML_file_debug, ML_file_no_debug} =
wenzelm@62902
     8
  ML_Compiler0.ML_file_operations (fn opt_debug => fn file =>
wenzelm@62817
     9
    let val flags = ML_Compiler.verbose true (ML_Compiler.debug_flags opt_debug) in
wenzelm@62817
    10
      ML_Context.eval_file flags (Path.explode file)
wenzelm@62817
    11
        handle ERROR msg => (writeln msg; error "ML error")
wenzelm@62817
    12
    end);
wenzelm@62944
    13
wenzelm@62944
    14
val use = ML_file;