1(*  Title:      Pure/ML/ml_compiler2.ML
2    Author:     Makarius
3
4Isabelle/ML file operations.
5*)
6
7val {ML_file, ML_file_debug, ML_file_no_debug} =
8  ML_Compiler0.ML_file_operations (fn opt_debug => fn file =>
9    let val flags = ML_Compiler.verbose true (ML_Compiler.debug_flags opt_debug) in
10      ML_Context.eval_file flags (Path.explode file)
11        handle ERROR msg => (writeln msg; error "ML error")
12    end);
13
14val use = ML_file;
15