added option ML_debugger;

--- a/etc/options	Thu Jul 16 11:10:57 2015 +0200
+++ b/etc/options	Thu Jul 16 11:38:18 2015 +0200
@@ -101,6 +101,9 @@
 public option ML_exception_trace : bool = false
   -- "ML exception trace for toplevel command execution"
 
+public option ML_debugger : bool = false
+  -- "ML debugger instrumentation for newly compiled code"
+
 public option ML_statistics : bool = true
   -- "ML runtime system statistics"
 

--- a/src/Pure/ML-Systems/ml_debugger_dummy.ML	Thu Jul 16 11:10:57 2015 +0200
+++ b/src/Pure/ML-Systems/ml_debugger_dummy.ML	Thu Jul 16 11:38:18 2015 +0200
@@ -6,8 +6,6 @@
 
 signature ML_DEBUGGER =
 sig
-  type compiler_parameters
-  val compiler_parameters: compiler_parameters
   type location
   val on_entry: (string * location -> unit) option -> unit
   val on_exit: (string * location -> unit) option -> unit
@@ -25,12 +23,6 @@
 structure ML_Debugger: ML_DEBUGGER =
 struct
 
-(* compiler parameters *)
-
-type compiler_parameters = unit;
-val compiler_parameters = ();
-
-
 (* hooks *)
 
 type location = unit;
@@ -54,3 +46,6 @@
 fun debug_name_space () = fail ();
 
 end;
+
+
+fun ml_debugger_parameters (_: bool) = [];

--- a/src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML	Thu Jul 16 11:10:57 2015 +0200
+++ b/src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML	Thu Jul 16 11:38:18 2015 +0200
@@ -7,12 +7,6 @@
 structure ML_Debugger: ML_DEBUGGER =
 struct
 
-(* compiler parameters *)
-
-type compiler_parameters = PolyML.Compiler.compilerParameters;
-val compiler_parameters = PolyML.Compiler.CPDebug true;
-
-
 (* hooks *)
 
 type location = PolyML.location;
@@ -35,3 +29,6 @@
 val debug_name_space = PolyML.DebuggerInterface.debugNameSpace;
 
 end;
+
+fun ml_debugger_parameters false = []
+  | ml_debugger_parameters true = [PolyML.Compiler.CPDebug true];

--- a/src/Pure/ML/ml_compiler_polyml.ML	Thu Jul 16 11:10:57 2015 +0200
+++ b/src/Pure/ML/ml_compiler_polyml.ML	Thu Jul 16 11:38:18 2015 +0200
@@ -183,7 +183,8 @@
       PolyML.Compiler.CPFileName location_props,
       PolyML.Compiler.CPPrintDepth ML_Options.get_print_depth,
       PolyML.Compiler.CPCompilerResultFun result_fun,
-      PolyML.Compiler.CPPrintInAlphabeticalOrder false];
+      PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
+     ml_debugger_parameters (ML_Options.debugger_enabled opt_context);
     val _ =
       (while not (List.null (! input_buffer)) do
         PolyML.compiler (get, parameters) ())

--- a/src/Pure/ML/ml_options.ML	Thu Jul 16 11:10:57 2015 +0200
+++ b/src/Pure/ML/ml_options.ML	Thu Jul 16 11:38:18 2015 +0200
@@ -11,6 +11,9 @@
   val exception_trace_raw: Config.raw
   val exception_trace: bool Config.T
   val exception_trace_enabled: Context.generic option -> bool
+  val debugger_raw: Config.raw
+  val debugger: bool Config.T
+  val debugger_enabled: Context.generic option -> bool
   val print_depth_raw: Config.raw
   val print_depth: int Config.T
   val get_print_depth: unit -> int
@@ -37,6 +40,16 @@
   | exception_trace_enabled (SOME context) = Config.get_generic context exception_trace;
 
 
+(* debugger *)
+
+val debugger_raw = Config.declare_option ("ML_debugger", @{here});
+val debugger = Config.bool debugger_raw;
+
+fun debugger_enabled NONE =
+      (Options.default_bool (Config.name_of debugger_raw) handle ERROR _ => false)
+  | debugger_enabled (SOME context) = Config.get_generic context debugger;
+
+
 (* print depth *)
 
 val print_depth_raw =