src/Pure/Tools/build.scala
changeset 62490 39d01eaf5292
parent 62486 b737f8f37454
child 62508 d0b68218ea55
--- a/src/Pure/Tools/build.scala	Tue Mar 01 17:26:53 2016 +0100
+++ b/src/Pure/Tools/build.scala	Tue Mar 01 19:42:59 2016 +0100
@@ -567,9 +567,15 @@
         }))
 
     private val env =
-      Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> output_standard_path,
-        (if (is_pure(name)) "ISABELLE_PROCESS_OPTIONS" else "ARGS_FILE") ->
-          File.standard_path(args_file))
+    {
+      val env0 =
+        Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> output_standard_path,
+          (if (is_pure(name)) "ISABELLE_PROCESS_OPTIONS" else "ARGS_FILE") ->
+            File.standard_path(args_file))
+      if (is_pure(name))
+        env0 + ("ISABELLE_ML_DEBUGGER" -> info.options.bool("ML_debugger").toString)
+      else env0
+    }
 
     private val script =
       """