src/Pure/ROOT.ML
changeset 62490 39d01eaf5292
parent 62459 7a5d88dd8cc9
child 62493 dd154240a53c
     1.1 --- a/src/Pure/ROOT.ML	Tue Mar 01 17:26:53 2016 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Tue Mar 01 19:42:59 2016 +0100
     1.3 @@ -39,11 +39,18 @@
     1.4  val use_text = Secure.use_text;
     1.5  val use_file = Secure.use_file;
     1.6  
     1.7 -fun use file =
     1.8 -  Position.setmp_thread_data (Position.file_only file)
     1.9 -    (fn () =>
    1.10 -      Secure.use_file ML_Parse.global_context {verbose = true, debug = false} file
    1.11 +local
    1.12 +  fun use_ opt_debug file =
    1.13 +    Position.setmp_thread_data (Position.file_only file)
    1.14 +      (fn () =>
    1.15 +        Secure.use_file ML_Parse.global_context
    1.16 +          {verbose = true, debug = use_debug_option opt_debug} file
    1.17          handle ERROR msg => (writeln msg; error "ML error")) ();
    1.18 +in
    1.19 +  val use = use_ NONE;
    1.20 +  val use_debug = use_ (SOME true);
    1.21 +  val use_no_debug = use_ (SOME false);
    1.22 +end;
    1.23  
    1.24  
    1.25  
    1.26 @@ -223,9 +230,19 @@
    1.27  use "ML/ml_context.ML";
    1.28  use "ML/ml_antiquotation.ML";
    1.29  
    1.30 -fun use s =
    1.31 -  ML_Context.eval_file (ML_Compiler.verbose true ML_Compiler.flags) (Path.explode s)
    1.32 -    handle ERROR msg => (writeln msg; error "ML error");
    1.33 +local
    1.34 +  fun use_ opt_debug file =
    1.35 +    let val flags = ML_Compiler.debug_flags opt_debug |> ML_Compiler.verbose true in
    1.36 +      ML_Context.eval_file flags (Path.explode file)
    1.37 +        handle ERROR msg => (writeln msg; error "ML error")
    1.38 +    end;
    1.39 +in
    1.40 +
    1.41 +val use = use_ NONE;
    1.42 +val use_debug = use_ (SOME true);
    1.43 +val use_no_debug = use_ (SOME false);
    1.44 +
    1.45 +end;
    1.46  
    1.47  
    1.48