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