src/Pure/ROOT.ML

--- a/src/Pure/ROOT.ML	Mon Aug 17 16:27:12 2015 +0200
+++ b/src/Pure/ROOT.ML	Mon Aug 17 19:34:15 2015 +0200
@@ -41,11 +41,23 @@
 val use_text = Secure.use_text;
 val use_file = Secure.use_file;
 
-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")) ();
+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);
 
 val toplevel_pp = Secure.toplevel_pp;
 
@@ -95,6 +107,8 @@
 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 *)
 
@@ -204,6 +218,10 @@
 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";
@@ -244,9 +262,21 @@
 use "ML/ml_context.ML";
 use "ML/ml_antiquotation.ML";
 
-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");
+local
+  fun use_ debug file =
+    let
+      val 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)
+        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;
 
 
 
@@ -377,4 +407,3 @@
 val cd = File.cd o Path.explode;
 
 Proofterm.proofs := 0;
-