src/Pure/ROOT.ML
changeset 60957 574254152856
parent 60956 10d463883dc2
child 60958 5d70b5c509f8
     1.1 --- a/src/Pure/ROOT.ML	Mon Aug 17 16:27:12 2015 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Mon Aug 17 19:34:15 2015 +0200
     1.3 @@ -41,11 +41,23 @@
     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 -        handle ERROR msg => (writeln msg; error "ML error")) ();
    1.12 +fun use_fns default_debug_option =
    1.13 +  let
    1.14 +    fun use_ debug_option file =
    1.15 +      let
    1.16 +        val debug =
    1.17 +          (case debug_option of
    1.18 +            SOME debug => debug
    1.19 +          | NONE => default_debug_option ());
    1.20 +      in
    1.21 +        Position.setmp_thread_data (Position.file_only file)
    1.22 +          (fn () =>
    1.23 +            Secure.use_file ML_Parse.global_context {verbose = true, debug = debug} file
    1.24 +              handle ERROR msg => (writeln msg; error "ML error")) ()
    1.25 +      end;
    1.26 +  in {use = use_ NONE, use_debug = use_ (SOME true), use_no_debug = use_ (SOME false)} end;
    1.27 +
    1.28 +val {use, use_debug, use_no_debug} = use_fns (K false);
    1.29  
    1.30  val toplevel_pp = Secure.toplevel_pp;
    1.31  
    1.32 @@ -95,6 +107,8 @@
    1.33  use "System/options.ML";
    1.34  use "config.ML";
    1.35  
    1.36 +val {use, use_debug, use_no_debug} = use_fns (fn () => Options.default_bool "ML_debugger");
    1.37 +
    1.38  
    1.39  (* concurrency within the ML runtime *)
    1.40  
    1.41 @@ -204,6 +218,10 @@
    1.42  use "ML/ml_syntax.ML";
    1.43  use "ML/ml_env.ML";
    1.44  use "ML/ml_options.ML";
    1.45 +
    1.46 +val {use, use_debug, use_no_debug} =
    1.47 +  use_fns (fn () => ML_Options.debugger_enabled (Context.thread_data ()));
    1.48 +
    1.49  use "ML/exn_output.ML";
    1.50  if ML_System.is_polyml then use "ML/exn_output_polyml.ML" else ();
    1.51  use "ML/ml_options.ML";
    1.52 @@ -244,9 +262,21 @@
    1.53  use "ML/ml_context.ML";
    1.54  use "ML/ml_antiquotation.ML";
    1.55  
    1.56 -fun use s =
    1.57 -  ML_Context.eval_file (ML_Compiler.verbose true ML_Compiler.flags) (Path.explode s)
    1.58 -    handle ERROR msg => (writeln msg; error "ML error");
    1.59 +local
    1.60 +  fun use_ debug file =
    1.61 +    let
    1.62 +      val flags =
    1.63 +        {SML = false, exchange = false, redirect = false, verbose = true,
    1.64 +          debug = debug, writeln = writeln, warning = warning};
    1.65 +    in
    1.66 +      ML_Context.eval_file (ML_Compiler.verbose true ML_Compiler.flags) (Path.explode file)
    1.67 +        handle ERROR msg => (writeln msg; error "ML error")
    1.68 +    end
    1.69 +in
    1.70 +  val use = use_ NONE;
    1.71 +  val use_debug = use_ (SOME true);
    1.72 +  val use_no_debug = use_ (SOME false);
    1.73 +end;
    1.74  
    1.75  
    1.76  
    1.77 @@ -377,4 +407,3 @@
    1.78  val cd = File.cd o Path.explode;
    1.79  
    1.80  Proofterm.proofs := 0;
    1.81 -