clarified ML bootstrap;
authorwenzelm
Sun Apr 06 15:19:22 2014 +0200 (2014-04-06)
changeset 564347acc933bd7cc
parent 56433 db69cb14f7ed
child 56435 28b34e8e4a80
clarified ML bootstrap;
src/Pure/General/secure.ML
src/Pure/ML/ml_context.ML
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/General/secure.ML	Sun Apr 06 14:30:26 2014 +0200
     1.2 +++ b/src/Pure/General/secure.ML	Sun Apr 06 15:19:22 2014 +0200
     1.3 @@ -58,15 +58,3 @@
     1.4  
     1.5  end;
     1.6  
     1.7 -(*override previous toplevel bindings!*)
     1.8 -val use_text = Secure.use_text;
     1.9 -val use_file = Secure.use_file;
    1.10 -
    1.11 -fun use s =
    1.12 -  Position.setmp_thread_data (Position.file_only s)
    1.13 -    (fn () =>
    1.14 -      Secure.use_file ML_Parse.global_context true s
    1.15 -        handle ERROR msg => (writeln msg; error "ML error")) ();
    1.16 -
    1.17 -val toplevel_pp = Secure.toplevel_pp;
    1.18 -
     2.1 --- a/src/Pure/ML/ml_context.ML	Sun Apr 06 14:30:26 2014 +0200
     2.2 +++ b/src/Pure/ML/ml_context.ML	Sun Apr 06 15:19:22 2014 +0200
     2.3 @@ -188,7 +188,3 @@
     2.4  
     2.5  end;
     2.6  
     2.7 -fun use s =
     2.8 -  ML_Context.eval_file (ML_Compiler.verbose true ML_Compiler.flags) (Path.explode s)
     2.9 -    handle ERROR msg => (writeln msg; error "ML error");
    2.10 -
     3.1 --- a/src/Pure/ROOT.ML	Sun Apr 06 14:30:26 2014 +0200
     3.2 +++ b/src/Pure/ROOT.ML	Sun Apr 06 15:19:22 2014 +0200
     3.3 @@ -38,6 +38,16 @@
     3.4  use "ML/ml_parse.ML";
     3.5  use "General/secure.ML";
     3.6  
     3.7 +val use_text = Secure.use_text;
     3.8 +val use_file = Secure.use_file;
     3.9 +
    3.10 +fun use s =
    3.11 +  Position.setmp_thread_data (Position.file_only s)
    3.12 +    (fn () =>
    3.13 +      Secure.use_file ML_Parse.global_context true s
    3.14 +        handle ERROR msg => (writeln msg; error "ML error")) ();
    3.15 +
    3.16 +val toplevel_pp = Secure.toplevel_pp;
    3.17  
    3.18  
    3.19  (** bootstrap phase 1: towards ML within Isar context *)
    3.20 @@ -236,6 +246,10 @@
    3.21  use "ML/ml_context.ML";
    3.22  use "ML/ml_antiquotation.ML";
    3.23  
    3.24 +fun use s =
    3.25 +  ML_Context.eval_file (ML_Compiler.verbose true ML_Compiler.flags) (Path.explode s)
    3.26 +    handle ERROR msg => (writeln msg; error "ML error");
    3.27 +
    3.28  
    3.29  
    3.30  (** bootstrap phase 2: towards Pure.thy and final ML toplevel setup *)