clarified ML compiler parameters: always provide PolyML.Compiler.CPDebug, ignore global default;
authorwenzelm
Fri Jul 17 16:43:53 2015 +0200 (2015-07-17)
changeset 60745d86b4cd0f1ec
parent 60744 4eba53a0ac3d
child 60746 8cf877aca29a
clarified ML compiler parameters: always provide PolyML.Compiler.CPDebug, ignore global default;
tuned;
src/Pure/ML-Systems/ml_compiler_parameters.ML
src/Pure/ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML
src/Pure/ML-Systems/ml_debugger.ML
src/Pure/ML-Systems/ml_debugger_dummy.ML
src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML
src/Pure/ML-Systems/polyml.ML
src/Pure/ML-Systems/smlnj.ML
src/Pure/ML/ml_compiler_polyml.ML
src/Pure/ROOT
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/ML-Systems/ml_compiler_parameters.ML	Fri Jul 17 16:43:53 2015 +0200
     1.3 @@ -0,0 +1,17 @@
     1.4 +(*  Title:      Pure/ML/ml_compiler_parameters.ML
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Additional ML compiler parameters for Poly/ML.
     1.8 +*)
     1.9 +
    1.10 +signature ML_COMPILER_PARAMETERS =
    1.11 +sig
    1.12 +  val debug: bool -> PolyML.Compiler.compilerParameters list
    1.13 +end;
    1.14 +
    1.15 +structure ML_Compiler_Parameters: ML_COMPILER_PARAMETERS =
    1.16 +struct
    1.17 +
    1.18 +fun debug _ = [];
    1.19 +
    1.20 +end;
    1.21 \ No newline at end of file
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML	Fri Jul 17 16:43:53 2015 +0200
     2.3 @@ -0,0 +1,12 @@
     2.4 +(*  Title:      Pure/ML/ml_compiler_parameters_polyml-5.5.3.ML
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Additional ML compiler parameters for Poly/ML 5.5.3, or later.
     2.8 +*)
     2.9 +
    2.10 +structure ML_Compiler_Parameters: ML_COMPILER_PARAMETERS =
    2.11 +struct
    2.12 +
    2.13 +fun debug b = [PolyML.Compiler.CPDebug b];
    2.14 +
    2.15 +end;
    2.16 \ No newline at end of file
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/ML-Systems/ml_debugger.ML	Fri Jul 17 16:43:53 2015 +0200
     3.3 @@ -0,0 +1,48 @@
     3.4 +(*  Title:      Pure/ML/ml_debugger.ML
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +ML debugger interface.
     3.8 +*)
     3.9 +
    3.10 +signature ML_DEBUGGER =
    3.11 +sig
    3.12 +  type location
    3.13 +  val on_entry: (string * location -> unit) option -> unit
    3.14 +  val on_exit: (string * location -> unit) option -> unit
    3.15 +  val on_exit_exception: (string * location -> exn -> unit) option -> unit
    3.16 +  val on_breakpoint: (location * bool Unsynchronized.ref -> unit) option -> unit
    3.17 +  type state
    3.18 +  val state: Thread.thread -> state list
    3.19 +  val debug_function: state -> string
    3.20 +  val debug_function_arg: state -> ML_Name_Space.valueVal
    3.21 +  val debug_function_result: state -> ML_Name_Space.valueVal
    3.22 +  val debug_location: state -> location
    3.23 +  val debug_name_space: state -> ML_Name_Space.T
    3.24 +end;
    3.25 +
    3.26 +structure ML_Debugger: ML_DEBUGGER =
    3.27 +struct
    3.28 +
    3.29 +(* hooks *)
    3.30 +
    3.31 +type location = unit;
    3.32 +fun on_entry _ = ();
    3.33 +fun on_exit _ = ();
    3.34 +fun on_exit_exception _ = ();
    3.35 +fun on_breakpoint _ = ();
    3.36 +
    3.37 +
    3.38 +(* debugger *)
    3.39 +
    3.40 +fun fail () = raise Fail "No debugger support on this ML platform";
    3.41 +
    3.42 +type state = unit;
    3.43 +
    3.44 +fun state _ = [];
    3.45 +fun debug_function () = fail ();
    3.46 +fun debug_function_arg () = fail ();
    3.47 +fun debug_function_result () = fail ();
    3.48 +fun debug_location () = fail ();
    3.49 +fun debug_name_space () = fail ();
    3.50 +
    3.51 +end;
     4.1 --- a/src/Pure/ML-Systems/ml_debugger_dummy.ML	Fri Jul 17 16:23:25 2015 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,51 +0,0 @@
     4.4 -(*  Title:      Pure/ML/ml_debugger_dummy.ML
     4.5 -    Author:     Makarius
     4.6 -
     4.7 -ML debugger interface -- dummy version.
     4.8 -*)
     4.9 -
    4.10 -signature ML_DEBUGGER =
    4.11 -sig
    4.12 -  type location
    4.13 -  val on_entry: (string * location -> unit) option -> unit
    4.14 -  val on_exit: (string * location -> unit) option -> unit
    4.15 -  val on_exit_exception: (string * location -> exn -> unit) option -> unit
    4.16 -  val on_breakpoint: (location * bool Unsynchronized.ref -> unit) option -> unit
    4.17 -  type state
    4.18 -  val state: Thread.thread -> state list
    4.19 -  val debug_function: state -> string
    4.20 -  val debug_function_arg: state -> ML_Name_Space.valueVal
    4.21 -  val debug_function_result: state -> ML_Name_Space.valueVal
    4.22 -  val debug_location: state -> location
    4.23 -  val debug_name_space: state -> ML_Name_Space.T
    4.24 -end;
    4.25 -
    4.26 -structure ML_Debugger: ML_DEBUGGER =
    4.27 -struct
    4.28 -
    4.29 -(* hooks *)
    4.30 -
    4.31 -type location = unit;
    4.32 -fun on_entry _ = ();
    4.33 -fun on_exit _ = ();
    4.34 -fun on_exit_exception _ = ();
    4.35 -fun on_breakpoint _ = ();
    4.36 -
    4.37 -
    4.38 -(* debugger *)
    4.39 -
    4.40 -fun fail () = raise Fail "No debugger support on this ML platform";
    4.41 -
    4.42 -type state = unit;
    4.43 -
    4.44 -fun state _ = [];
    4.45 -fun debug_function () = fail ();
    4.46 -fun debug_function_arg () = fail ();
    4.47 -fun debug_function_result () = fail ();
    4.48 -fun debug_location () = fail ();
    4.49 -fun debug_name_space () = fail ();
    4.50 -
    4.51 -end;
    4.52 -
    4.53 -
    4.54 -fun ml_debugger_parameters (_: bool) = [];
     5.1 --- a/src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML	Fri Jul 17 16:23:25 2015 +0200
     5.2 +++ b/src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML	Fri Jul 17 16:43:53 2015 +0200
     5.3 @@ -29,6 +29,3 @@
     5.4  val debug_name_space = PolyML.DebuggerInterface.debugNameSpace;
     5.5  
     5.6  end;
     5.7 -
     5.8 -fun ml_debugger_parameters false = []
     5.9 -  | ml_debugger_parameters true = [PolyML.Compiler.CPDebug true];
     6.1 --- a/src/Pure/ML-Systems/polyml.ML	Fri Jul 17 16:23:25 2015 +0200
     6.2 +++ b/src/Pure/ML-Systems/polyml.ML	Fri Jul 17 16:43:53 2015 +0200
     6.3 @@ -133,12 +133,17 @@
     6.4  fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
     6.5  
     6.6  use "ML-Systems/ml_parse_tree.ML";
     6.7 -if ML_System.name = "polyml-5.5.3" then use "ML-Systems/ml_parse_tree_polyml-5.5.3.ML" else ();
     6.8 +if ML_System.name = "polyml-5.5.3"
     6.9 +then use "ML-Systems/ml_parse_tree_polyml-5.5.3.ML" else ();
    6.10 +
    6.11 +use "ML-Systems/ml_compiler_parameters.ML";
    6.12 +if ML_System.name = "polyml-5.5.3"
    6.13 +then use "ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML" else ();
    6.14  
    6.15  
    6.16  (* ML debugger *)
    6.17  
    6.18 -use "ML-Systems/ml_debugger_dummy.ML";
    6.19 +use "ML-Systems/ml_debugger.ML";
    6.20  if ML_System.name = "polyml-5.5.3" then use "ML-Systems/ml_debugger_polyml-5.5.3.ML" else ();
    6.21  
    6.22  
     7.1 --- a/src/Pure/ML-Systems/smlnj.ML	Fri Jul 17 16:23:25 2015 +0200
     7.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Fri Jul 17 16:43:53 2015 +0200
     7.3 @@ -162,7 +162,7 @@
     7.4  
     7.5  
     7.6  use "ML-Systems/unsynchronized.ML";
     7.7 -use "ML-Systems/ml_debugger_dummy.ML";
     7.8 +use "ML-Systems/ml_debugger.ML";
     7.9  
    7.10  
    7.11  (* ML system operations *)
     8.1 --- a/src/Pure/ML/ml_compiler_polyml.ML	Fri Jul 17 16:23:25 2015 +0200
     8.2 +++ b/src/Pure/ML/ml_compiler_polyml.ML	Fri Jul 17 16:43:53 2015 +0200
     8.3 @@ -223,7 +223,7 @@
     8.4        PolyML.Compiler.CPPrintDepth ML_Options.get_print_depth,
     8.5        PolyML.Compiler.CPCompilerResultFun result_fun,
     8.6        PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
     8.7 -     ml_debugger_parameters (ML_Options.debugger_enabled opt_context);
     8.8 +     ML_Compiler_Parameters.debug (ML_Options.debugger_enabled opt_context);
     8.9      val _ =
    8.10        (while not (List.null (! input_buffer)) do
    8.11          PolyML.compiler (get, parameters) ())
     9.1 --- a/src/Pure/ROOT	Fri Jul 17 16:23:25 2015 +0200
     9.2 +++ b/src/Pure/ROOT	Fri Jul 17 16:43:53 2015 +0200
     9.3 @@ -6,7 +6,9 @@
     9.4      "General/exn.ML"
     9.5      "ML-Systems/compiler_polyml.ML"
     9.6      "ML-Systems/exn_trace_polyml-5.5.1.ML"
     9.7 -    "ML-Systems/ml_debugger_dummy.ML"
     9.8 +    "ML-Systems/ml_compiler_parameters.ML"
     9.9 +    "ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML"
    9.10 +    "ML-Systems/ml_debugger.ML"
    9.11      "ML-Systems/ml_debugger_polyml-5.5.3.ML"
    9.12      "ML-Systems/ml_name_space.ML"
    9.13      "ML-Systems/ml_parse_tree.ML"
    9.14 @@ -37,7 +39,9 @@
    9.15      "General/exn.ML"
    9.16      "ML-Systems/compiler_polyml.ML"
    9.17      "ML-Systems/exn_trace_polyml-5.5.1.ML"
    9.18 -    "ML-Systems/ml_debugger_dummy.ML"
    9.19 +    "ML-Systems/ml_compiler_parameters.ML"
    9.20 +    "ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML"
    9.21 +    "ML-Systems/ml_debugger.ML"
    9.22      "ML-Systems/ml_debugger_polyml-5.5.3.ML"
    9.23      "ML-Systems/ml_name_space.ML"
    9.24      "ML-Systems/ml_parse_tree.ML"