# HG changeset patch
# User wenzelm
# Date 1439839375 -7200
# Node ID 5d70b5c509f82cdbecb8f72a835892ddbe098590
# Parent  574254152856be599e3a93346af9832f9dbe7e59
more careful propagation of ML_debugger option to Pure;

diff -r 574254152856 -r 5d70b5c509f8 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Aug 17 19:34:15 2015 +0200
+++ b/src/Pure/ROOT.ML	Mon Aug 17 21:22:55 2015 +0200
@@ -41,23 +41,24 @@
 val use_text = Secure.use_text;
 val use_file = Secure.use_file;
 
-fun use_fns default_debug_option =
-  let
-    fun use_ debug_option file =
-      let
-        val debug =
-          (case debug_option of
-            SOME debug => debug
-          | NONE => default_debug_option ());
-      in
-        Position.setmp_thread_data (Position.file_only file)
-          (fn () =>
-            Secure.use_file ML_Parse.global_context {verbose = true, debug = debug} file
-              handle ERROR msg => (writeln msg; error "ML error")) ()
-      end;
-  in {use = use_ NONE, use_debug = use_ (SOME true), use_no_debug = use_ (SOME false)} end;
-
-val {use, use_debug, use_no_debug} = use_fns (K false);
+local
+  fun use_ debug_option file =
+    let
+      val debug =
+        (case debug_option of
+          SOME debug => debug
+        | NONE => getenv "ISABELLE_ML_DEBUGGER" = "true");
+    in
+      Position.setmp_thread_data (Position.file_only file)
+        (fn () =>
+          Secure.use_file ML_Parse.global_context {verbose = true, debug = debug} file
+            handle ERROR msg => (writeln msg; error "ML error")) ()
+    end;
+in
+  val use = use_ NONE;
+  val use_debug = use_ (SOME true);
+  val use_no_debug = use_ (SOME false);
+end;
 
 val toplevel_pp = Secure.toplevel_pp;
 
@@ -107,8 +108,6 @@
 use "System/options.ML";
 use "config.ML";
 
-val {use, use_debug, use_no_debug} = use_fns (fn () => Options.default_bool "ML_debugger");
-
 
 (* concurrency within the ML runtime *)
 
@@ -218,10 +217,6 @@
 use "ML/ml_syntax.ML";
 use "ML/ml_env.ML";
 use "ML/ml_options.ML";
-
-val {use, use_debug, use_no_debug} =
-  use_fns (fn () => ML_Options.debugger_enabled (Context.thread_data ()));
-
 use "ML/exn_output.ML";
 if ML_System.is_polyml then use "ML/exn_output_polyml.ML" else ();
 use "ML/ml_options.ML";
@@ -265,13 +260,13 @@
 local
   fun use_ debug file =
     let
-      val flags =
+      val flags: ML_Compiler.flags =
         {SML = false, exchange = false, redirect = false, verbose = true,
           debug = debug, writeln = writeln, warning = warning};
     in
-      ML_Context.eval_file (ML_Compiler.verbose true ML_Compiler.flags) (Path.explode file)
+      ML_Context.eval_file flags (Path.explode file)
         handle ERROR msg => (writeln msg; error "ML error")
-    end
+    end;
 in
   val use = use_ NONE;
   val use_debug = use_ (SOME true);
diff -r 574254152856 -r 5d70b5c509f8 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Aug 17 19:34:15 2015 +0200
+++ b/src/Pure/Tools/build.scala	Mon Aug 17 21:22:55 2015 +0200
@@ -590,11 +590,16 @@
                 (info.chapter, (name, theories)))))))))))
         }))
 
-    private val env =
+    private val env0 =
       Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> Isabelle_System.standard_path(output),
         (if (is_pure(name)) "ISABELLE_PROCESS_OPTIONS" else "ARGS_FILE") ->
           Isabelle_System.posix_path(args_file))
 
+    private val env =
+      if (is_pure(name))
+        env0 + ("ISABELLE_ML_DEBUGGER" -> info.options.bool("ML_debugger").toString)
+      else env0
+
     private val script =
       if (is_pure(name)) {
         if (do_output) "./build " + name + " \"$OUTPUT\""