src/Pure/ROOT.ML
changeset 62494 b90109b2487c
parent 62493 dd154240a53c
child 62498 5dfcc9697f29
     1.1 --- a/src/Pure/ROOT.ML	Tue Mar 01 21:10:29 2016 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Tue Mar 01 22:11:36 2016 +0100
     1.3 @@ -36,17 +36,18 @@
     1.4  
     1.5  val {use, use_debug, use_no_debug} =
     1.6    let
     1.7 -    val global_context: use_context =
     1.8 +    val context: ML_Compiler0.context =
     1.9       {name_space = ML_Name_Space.global,
    1.10        here = Position.here oo Position.line_file,
    1.11        print = writeln,
    1.12 -      error = error}
    1.13 +      error = error};
    1.14    in
    1.15 -    use_operations (fn opt_debug => fn file =>
    1.16 +    ML_Compiler0.use_operations (fn opt_debug => fn file =>
    1.17        Position.setmp_thread_data (Position.file_only file)
    1.18          (fn () =>
    1.19 -          use_file global_context {verbose = true, debug = use_debug_option opt_debug} file
    1.20 -            handle ERROR msg => (writeln msg; error "ML error")) ())
    1.21 +          ML_Compiler0.use_file context
    1.22 +            {verbose = true, debug = ML_Compiler0.debug_option opt_debug} file
    1.23 +          handle ERROR msg => (writeln msg; error "ML error")) ())
    1.24    end;
    1.25  
    1.26  
    1.27 @@ -228,7 +229,7 @@
    1.28  use "ML/ml_antiquotation.ML";
    1.29  
    1.30  val {use, use_debug, use_no_debug} =
    1.31 -  use_operations (fn opt_debug => fn file =>
    1.32 +  ML_Compiler0.use_operations (fn opt_debug => fn file =>
    1.33      let val flags = ML_Compiler.verbose true (ML_Compiler.debug_flags opt_debug) in
    1.34        ML_Context.eval_file flags (Path.explode file)
    1.35          handle ERROR msg => (writeln msg; error "ML error")