more careful propagation of ML_debugger option to Pure;
authorwenzelm
Mon Aug 17 21:22:55 2015 +0200 (2015-08-17)
changeset 609585d70b5c509f8
parent 60957 574254152856
child 60959 3565c9f407ec
more careful propagation of ML_debugger option to Pure;
src/Pure/ROOT.ML
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/ROOT.ML	Mon Aug 17 19:34:15 2015 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Mon Aug 17 21:22:55 2015 +0200
     1.3 @@ -41,23 +41,24 @@
     1.4  val use_text = Secure.use_text;
     1.5  val use_file = Secure.use_file;
     1.6  
     1.7 -fun use_fns default_debug_option =
     1.8 -  let
     1.9 -    fun use_ debug_option file =
    1.10 -      let
    1.11 -        val debug =
    1.12 -          (case debug_option of
    1.13 -            SOME debug => debug
    1.14 -          | NONE => default_debug_option ());
    1.15 -      in
    1.16 -        Position.setmp_thread_data (Position.file_only file)
    1.17 -          (fn () =>
    1.18 -            Secure.use_file ML_Parse.global_context {verbose = true, debug = debug} file
    1.19 -              handle ERROR msg => (writeln msg; error "ML error")) ()
    1.20 -      end;
    1.21 -  in {use = use_ NONE, use_debug = use_ (SOME true), use_no_debug = use_ (SOME false)} end;
    1.22 -
    1.23 -val {use, use_debug, use_no_debug} = use_fns (K false);
    1.24 +local
    1.25 +  fun use_ debug_option file =
    1.26 +    let
    1.27 +      val debug =
    1.28 +        (case debug_option of
    1.29 +          SOME debug => debug
    1.30 +        | NONE => getenv "ISABELLE_ML_DEBUGGER" = "true");
    1.31 +    in
    1.32 +      Position.setmp_thread_data (Position.file_only file)
    1.33 +        (fn () =>
    1.34 +          Secure.use_file ML_Parse.global_context {verbose = true, debug = debug} file
    1.35 +            handle ERROR msg => (writeln msg; error "ML error")) ()
    1.36 +    end;
    1.37 +in
    1.38 +  val use = use_ NONE;
    1.39 +  val use_debug = use_ (SOME true);
    1.40 +  val use_no_debug = use_ (SOME false);
    1.41 +end;
    1.42  
    1.43  val toplevel_pp = Secure.toplevel_pp;
    1.44  
    1.45 @@ -107,8 +108,6 @@
    1.46  use "System/options.ML";
    1.47  use "config.ML";
    1.48  
    1.49 -val {use, use_debug, use_no_debug} = use_fns (fn () => Options.default_bool "ML_debugger");
    1.50 -
    1.51  
    1.52  (* concurrency within the ML runtime *)
    1.53  
    1.54 @@ -218,10 +217,6 @@
    1.55  use "ML/ml_syntax.ML";
    1.56  use "ML/ml_env.ML";
    1.57  use "ML/ml_options.ML";
    1.58 -
    1.59 -val {use, use_debug, use_no_debug} =
    1.60 -  use_fns (fn () => ML_Options.debugger_enabled (Context.thread_data ()));
    1.61 -
    1.62  use "ML/exn_output.ML";
    1.63  if ML_System.is_polyml then use "ML/exn_output_polyml.ML" else ();
    1.64  use "ML/ml_options.ML";
    1.65 @@ -265,13 +260,13 @@
    1.66  local
    1.67    fun use_ debug file =
    1.68      let
    1.69 -      val flags =
    1.70 +      val flags: ML_Compiler.flags =
    1.71          {SML = false, exchange = false, redirect = false, verbose = true,
    1.72            debug = debug, writeln = writeln, warning = warning};
    1.73      in
    1.74 -      ML_Context.eval_file (ML_Compiler.verbose true ML_Compiler.flags) (Path.explode file)
    1.75 +      ML_Context.eval_file flags (Path.explode file)
    1.76          handle ERROR msg => (writeln msg; error "ML error")
    1.77 -    end
    1.78 +    end;
    1.79  in
    1.80    val use = use_ NONE;
    1.81    val use_debug = use_ (SOME true);
     2.1 --- a/src/Pure/Tools/build.scala	Mon Aug 17 19:34:15 2015 +0200
     2.2 +++ b/src/Pure/Tools/build.scala	Mon Aug 17 21:22:55 2015 +0200
     2.3 @@ -590,11 +590,16 @@
     2.4                  (info.chapter, (name, theories)))))))))))
     2.5          }))
     2.6  
     2.7 -    private val env =
     2.8 +    private val env0 =
     2.9        Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> Isabelle_System.standard_path(output),
    2.10          (if (is_pure(name)) "ISABELLE_PROCESS_OPTIONS" else "ARGS_FILE") ->
    2.11            Isabelle_System.posix_path(args_file))
    2.12  
    2.13 +    private val env =
    2.14 +      if (is_pure(name))
    2.15 +        env0 + ("ISABELLE_ML_DEBUGGER" -> info.options.bool("ML_debugger").toString)
    2.16 +      else env0
    2.17 +
    2.18      private val script =
    2.19        if (is_pure(name)) {
    2.20          if (do_output) "./build " + name + " \"$OUTPUT\""