1(* Title: Pure/ML/ml_compiler1.ML 2 Author: Makarius 3 4Refined ML file operations for bootstrap. 5*) 6 7val {ML_file, ML_file_debug, ML_file_no_debug} = 8 let 9 val context: ML_Compiler0.context = 10 {name_space = ML_Name_Space.global, 11 print_depth = NONE, 12 here = Position.here oo Position.line_file, 13 print = writeln, 14 error = error}; 15 in 16 ML_Compiler0.ML_file_operations (fn opt_debug => fn file => 17 Position.setmp_thread_data (Position.file_only file) 18 (fn () => 19 ML_Compiler0.ML_file context 20 {verbose = true, debug = ML_Compiler0.debug_option opt_debug} file 21 handle ERROR msg => (writeln msg; error "ML error")) ()) 22 end; 23