src/Pure/ROOT.ML
changeset 62490 39d01eaf5292
parent 62459 7a5d88dd8cc9
child 62493 dd154240a53c
equal deleted inserted replaced
62489:36f11bc393a2 62490:39d01eaf5292
    37 use "General/secure.ML";
    37 use "General/secure.ML";
    38 
    38 
    39 val use_text = Secure.use_text;
    39 val use_text = Secure.use_text;
    40 val use_file = Secure.use_file;
    40 val use_file = Secure.use_file;
    41 
    41 
    42 fun use file =
    42 local
    43   Position.setmp_thread_data (Position.file_only file)
    43   fun use_ opt_debug file =
    44     (fn () =>
    44     Position.setmp_thread_data (Position.file_only file)
    45       Secure.use_file ML_Parse.global_context {verbose = true, debug = false} file
    45       (fn () =>
       
    46         Secure.use_file ML_Parse.global_context
       
    47           {verbose = true, debug = use_debug_option opt_debug} file
    46         handle ERROR msg => (writeln msg; error "ML error")) ();
    48         handle ERROR msg => (writeln msg; error "ML error")) ();
       
    49 in
       
    50   val use = use_ NONE;
       
    51   val use_debug = use_ (SOME true);
       
    52   val use_no_debug = use_ (SOME false);
       
    53 end;
    47 
    54 
    48 
    55 
    49 
    56 
    50 (** bootstrap phase 1: towards ML within Isar context *)
    57 (** bootstrap phase 1: towards ML within Isar context *)
    51 
    58 
   221 
   228 
   222 (*ML with context and antiquotations*)
   229 (*ML with context and antiquotations*)
   223 use "ML/ml_context.ML";
   230 use "ML/ml_context.ML";
   224 use "ML/ml_antiquotation.ML";
   231 use "ML/ml_antiquotation.ML";
   225 
   232 
   226 fun use s =
   233 local
   227   ML_Context.eval_file (ML_Compiler.verbose true ML_Compiler.flags) (Path.explode s)
   234   fun use_ opt_debug file =
   228     handle ERROR msg => (writeln msg; error "ML error");
   235     let val flags = ML_Compiler.debug_flags opt_debug |> ML_Compiler.verbose true in
       
   236       ML_Context.eval_file flags (Path.explode file)
       
   237         handle ERROR msg => (writeln msg; error "ML error")
       
   238     end;
       
   239 in
       
   240 
       
   241 val use = use_ NONE;
       
   242 val use_debug = use_ (SOME true);
       
   243 val use_no_debug = use_ (SOME false);
       
   244 
       
   245 end;
   229 
   246 
   230 
   247 
   231 
   248 
   232 (** bootstrap phase 2: towards Pure.thy and final ML toplevel setup *)
   249 (** bootstrap phase 2: towards Pure.thy and final ML toplevel setup *)
   233 
   250