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