clarified ML compiler parameters: always provide PolyML.Compiler.CPDebug, ignore global default;
tuned;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/ml_compiler_parameters.ML	Fri Jul 17 16:43:53 2015 +0200
@@ -0,0 +1,17 @@
+(*  Title:      Pure/ML/ml_compiler_parameters.ML
+    Author:     Makarius
+
+Additional ML compiler parameters for Poly/ML.
+*)
+
+signature ML_COMPILER_PARAMETERS =
+sig
+  val debug: bool -> PolyML.Compiler.compilerParameters list
+end;
+
+structure ML_Compiler_Parameters: ML_COMPILER_PARAMETERS =
+struct
+
+fun debug _ = [];
+
+end;
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML	Fri Jul 17 16:43:53 2015 +0200
@@ -0,0 +1,12 @@
+(*  Title:      Pure/ML/ml_compiler_parameters_polyml-5.5.3.ML
+    Author:     Makarius
+
+Additional ML compiler parameters for Poly/ML 5.5.3, or later.
+*)
+
+structure ML_Compiler_Parameters: ML_COMPILER_PARAMETERS =
+struct
+
+fun debug b = [PolyML.Compiler.CPDebug b];
+
+end;
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/ml_debugger.ML	Fri Jul 17 16:43:53 2015 +0200
@@ -0,0 +1,48 @@
+(*  Title:      Pure/ML/ml_debugger.ML
+    Author:     Makarius
+
+ML debugger interface.
+*)
+
+signature ML_DEBUGGER =
+sig
+  type location
+  val on_entry: (string * location -> unit) option -> unit
+  val on_exit: (string * location -> unit) option -> unit
+  val on_exit_exception: (string * location -> exn -> unit) option -> unit
+  val on_breakpoint: (location * bool Unsynchronized.ref -> unit) option -> unit
+  type state
+  val state: Thread.thread -> state list
+  val debug_function: state -> string
+  val debug_function_arg: state -> ML_Name_Space.valueVal
+  val debug_function_result: state -> ML_Name_Space.valueVal
+  val debug_location: state -> location
+  val debug_name_space: state -> ML_Name_Space.T
+end;
+
+structure ML_Debugger: ML_DEBUGGER =
+struct
+
+(* hooks *)
+
+type location = unit;
+fun on_entry _ = ();
+fun on_exit _ = ();
+fun on_exit_exception _ = ();
+fun on_breakpoint _ = ();
+
+
+(* debugger *)
+
+fun fail () = raise Fail "No debugger support on this ML platform";
+
+type state = unit;
+
+fun state _ = [];
+fun debug_function () = fail ();
+fun debug_function_arg () = fail ();
+fun debug_function_result () = fail ();
+fun debug_location () = fail ();
+fun debug_name_space () = fail ();
+
+end;

--- a/src/Pure/ML-Systems/ml_debugger_dummy.ML	Fri Jul 17 16:23:25 2015 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,51 +0,0 @@
-(*  Title:      Pure/ML/ml_debugger_dummy.ML
-    Author:     Makarius
-
-ML debugger interface -- dummy version.
-*)
-
-signature ML_DEBUGGER =
-sig
-  type location
-  val on_entry: (string * location -> unit) option -> unit
-  val on_exit: (string * location -> unit) option -> unit
-  val on_exit_exception: (string * location -> exn -> unit) option -> unit
-  val on_breakpoint: (location * bool Unsynchronized.ref -> unit) option -> unit
-  type state
-  val state: Thread.thread -> state list
-  val debug_function: state -> string
-  val debug_function_arg: state -> ML_Name_Space.valueVal
-  val debug_function_result: state -> ML_Name_Space.valueVal
-  val debug_location: state -> location
-  val debug_name_space: state -> ML_Name_Space.T
-end;
-
-structure ML_Debugger: ML_DEBUGGER =
-struct
-
-(* hooks *)
-
-type location = unit;
-fun on_entry _ = ();
-fun on_exit _ = ();
-fun on_exit_exception _ = ();
-fun on_breakpoint _ = ();
-
-
-(* debugger *)
-
-fun fail () = raise Fail "No debugger support on this ML platform";
-
-type state = unit;
-
-fun state _ = [];
-fun debug_function () = fail ();
-fun debug_function_arg () = fail ();
-fun debug_function_result () = fail ();
-fun debug_location () = fail ();
-fun debug_name_space () = fail ();
-
-end;
-
-
-fun ml_debugger_parameters (_: bool) = [];

--- a/src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML	Fri Jul 17 16:23:25 2015 +0200
+++ b/src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML	Fri Jul 17 16:43:53 2015 +0200
@@ -29,6 +29,3 @@
 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-Systems/polyml.ML	Fri Jul 17 16:23:25 2015 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Fri Jul 17 16:43:53 2015 +0200
@@ -133,12 +133,17 @@
 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
 
 use "ML-Systems/ml_parse_tree.ML";
-if ML_System.name = "polyml-5.5.3" then use "ML-Systems/ml_parse_tree_polyml-5.5.3.ML" else ();
+if ML_System.name = "polyml-5.5.3"
+then use "ML-Systems/ml_parse_tree_polyml-5.5.3.ML" else ();
+
+use "ML-Systems/ml_compiler_parameters.ML";
+if ML_System.name = "polyml-5.5.3"
+then use "ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML" else ();
 
 
 (* ML debugger *)
 
-use "ML-Systems/ml_debugger_dummy.ML";
+use "ML-Systems/ml_debugger.ML";
 if ML_System.name = "polyml-5.5.3" then use "ML-Systems/ml_debugger_polyml-5.5.3.ML" else ();
 
 

--- a/src/Pure/ML-Systems/smlnj.ML	Fri Jul 17 16:23:25 2015 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Fri Jul 17 16:43:53 2015 +0200
@@ -162,7 +162,7 @@
 
 
 use "ML-Systems/unsynchronized.ML";
-use "ML-Systems/ml_debugger_dummy.ML";
+use "ML-Systems/ml_debugger.ML";
 
 
 (* ML system operations *)

--- a/src/Pure/ML/ml_compiler_polyml.ML	Fri Jul 17 16:23:25 2015 +0200
+++ b/src/Pure/ML/ml_compiler_polyml.ML	Fri Jul 17 16:43:53 2015 +0200
@@ -223,7 +223,7 @@
       PolyML.Compiler.CPPrintDepth ML_Options.get_print_depth,
       PolyML.Compiler.CPCompilerResultFun result_fun,
       PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
-     ml_debugger_parameters (ML_Options.debugger_enabled opt_context);
+     ML_Compiler_Parameters.debug (ML_Options.debugger_enabled opt_context);
     val _ =
       (while not (List.null (! input_buffer)) do
         PolyML.compiler (get, parameters) ())

--- a/src/Pure/ROOT	Fri Jul 17 16:23:25 2015 +0200
+++ b/src/Pure/ROOT	Fri Jul 17 16:43:53 2015 +0200
@@ -6,7 +6,9 @@
     "General/exn.ML"
     "ML-Systems/compiler_polyml.ML"
     "ML-Systems/exn_trace_polyml-5.5.1.ML"
-    "ML-Systems/ml_debugger_dummy.ML"
+    "ML-Systems/ml_compiler_parameters.ML"
+    "ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML"
+    "ML-Systems/ml_debugger.ML"
     "ML-Systems/ml_debugger_polyml-5.5.3.ML"
     "ML-Systems/ml_name_space.ML"
     "ML-Systems/ml_parse_tree.ML"
@@ -37,7 +39,9 @@
     "General/exn.ML"
     "ML-Systems/compiler_polyml.ML"
     "ML-Systems/exn_trace_polyml-5.5.1.ML"
-    "ML-Systems/ml_debugger_dummy.ML"
+    "ML-Systems/ml_compiler_parameters.ML"
+    "ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML"
+    "ML-Systems/ml_debugger.ML"
     "ML-Systems/ml_debugger_polyml-5.5.3.ML"
     "ML-Systems/ml_name_space.ML"
     "ML-Systems/ml_parse_tree.ML"