src/Pure/ROOT.ML
changeset 62493 dd154240a53c
parent 62490 39d01eaf5292
child 62494 b90109b2487c
     1.1 --- a/src/Pure/ROOT.ML	Tue Mar 01 21:00:38 2016 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Tue Mar 01 21:10:29 2016 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4  (*** Isabelle/Pure bootstrap from "RAW" environment ***)
     1.5  
     1.6 -(** bootstrap phase 0: towards secure ML barrier *)
     1.7 +(** bootstrap phase 0: towards ML within position context *)
     1.8  
     1.9  structure Distribution =     (*filled-in by makedist*)
    1.10  struct
    1.11 @@ -33,24 +33,21 @@
    1.12  use "General/input.ML";
    1.13  use "General/antiquote.ML";
    1.14  use "ML/ml_lex.ML";
    1.15 -use "ML/ml_parse.ML";
    1.16 -use "General/secure.ML";
    1.17  
    1.18 -val use_text = Secure.use_text;
    1.19 -val use_file = Secure.use_file;
    1.20 -
    1.21 -local
    1.22 -  fun use_ opt_debug file =
    1.23 -    Position.setmp_thread_data (Position.file_only file)
    1.24 -      (fn () =>
    1.25 -        Secure.use_file ML_Parse.global_context
    1.26 -          {verbose = true, debug = use_debug_option opt_debug} file
    1.27 -        handle ERROR msg => (writeln msg; error "ML error")) ();
    1.28 -in
    1.29 -  val use = use_ NONE;
    1.30 -  val use_debug = use_ (SOME true);
    1.31 -  val use_no_debug = use_ (SOME false);
    1.32 -end;
    1.33 +val {use, use_debug, use_no_debug} =
    1.34 +  let
    1.35 +    val global_context: use_context =
    1.36 +     {name_space = ML_Name_Space.global,
    1.37 +      here = Position.here oo Position.line_file,
    1.38 +      print = writeln,
    1.39 +      error = error}
    1.40 +  in
    1.41 +    use_operations (fn opt_debug => fn file =>
    1.42 +      Position.setmp_thread_data (Position.file_only file)
    1.43 +        (fn () =>
    1.44 +          use_file global_context {verbose = true, debug = use_debug_option opt_debug} file
    1.45 +            handle ERROR msg => (writeln msg; error "ML error")) ())
    1.46 +  end;
    1.47  
    1.48  
    1.49  
    1.50 @@ -230,19 +227,12 @@
    1.51  use "ML/ml_context.ML";
    1.52  use "ML/ml_antiquotation.ML";
    1.53  
    1.54 -local
    1.55 -  fun use_ opt_debug file =
    1.56 -    let val flags = ML_Compiler.debug_flags opt_debug |> ML_Compiler.verbose true in
    1.57 +val {use, use_debug, use_no_debug} =
    1.58 +  use_operations (fn opt_debug => fn file =>
    1.59 +    let val flags = ML_Compiler.verbose true (ML_Compiler.debug_flags opt_debug) in
    1.60        ML_Context.eval_file flags (Path.explode file)
    1.61          handle ERROR msg => (writeln msg; error "ML error")
    1.62 -    end;
    1.63 -in
    1.64 -
    1.65 -val use = use_ NONE;
    1.66 -val use_debug = use_ (SOME true);
    1.67 -val use_no_debug = use_ (SOME false);
    1.68 -
    1.69 -end;
    1.70 +    end);
    1.71  
    1.72  
    1.73