src/Pure/ML/ml_compiler1.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 62902 3c0f53eae166
permissions -rw-r--r--
more robust sorted_entries;
     1 (*  Title:      Pure/ML/ml_compiler1.ML
     2     Author:     Makarius
     3 
     4 Refined ML file operations for bootstrap.
     5 *)
     6 
     7 val {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;