no ML_debugger support in Pure -- too complicated;

--- a/src/Pure/ROOT.ML	Mon Aug 17 21:22:55 2015 +0200
+++ b/src/Pure/ROOT.ML	Mon Aug 17 21:32:41 2015 +0200
@@ -41,24 +41,11 @@
 val use_text = Secure.use_text;
 val use_file = Secure.use_file;
 
-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;
+fun use file =
+  Position.setmp_thread_data (Position.file_only file)
+    (fn () =>
+      Secure.use_file ML_Parse.global_context {verbose = true, debug = false} file
+        handle ERROR msg => (writeln msg; error "ML error")) ();
 
 val toplevel_pp = Secure.toplevel_pp;
 
@@ -257,21 +244,9 @@
 use "ML/ml_context.ML";
 use "ML/ml_antiquotation.ML";
 
-local
-  fun use_ debug file =
-    let
-      val flags: ML_Compiler.flags =
-        {SML = false, exchange = false, redirect = false, verbose = true,
-          debug = debug, writeln = writeln, warning = warning};
-    in
-      ML_Context.eval_file flags (Path.explode 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;
+fun use s =
+  ML_Context.eval_file (ML_Compiler.verbose true ML_Compiler.flags) (Path.explode s)
+    handle ERROR msg => (writeln msg; error "ML error");
 
 
 

--- a/src/Pure/Tools/build.scala	Mon Aug 17 21:22:55 2015 +0200
+++ b/src/Pure/Tools/build.scala	Mon Aug 17 21:32:41 2015 +0200
@@ -590,16 +590,11 @@
                 (info.chapter, (name, theories)))))))))))
         }))
 
-    private val env0 =
+    private val env =
       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\""