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