added option ML_debugger;
authorwenzelm
Thu Jul 16 11:38:18 2015 +0200 (2015-07-16)
changeset 6073002c2860fcf30
parent 60729 f5989a2c1f67
child 60731 4ac4b314d93c
added option ML_debugger;
etc/options
src/Pure/ML-Systems/ml_debugger_dummy.ML
src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML
src/Pure/ML/ml_compiler_polyml.ML
src/Pure/ML/ml_options.ML
     1.1 --- a/etc/options	Thu Jul 16 11:10:57 2015 +0200
     1.2 +++ b/etc/options	Thu Jul 16 11:38:18 2015 +0200
     1.3 @@ -101,6 +101,9 @@
     1.4  public option ML_exception_trace : bool = false
     1.5    -- "ML exception trace for toplevel command execution"
     1.6  
     1.7 +public option ML_debugger : bool = false
     1.8 +  -- "ML debugger instrumentation for newly compiled code"
     1.9 +
    1.10  public option ML_statistics : bool = true
    1.11    -- "ML runtime system statistics"
    1.12  
     2.1 --- a/src/Pure/ML-Systems/ml_debugger_dummy.ML	Thu Jul 16 11:10:57 2015 +0200
     2.2 +++ b/src/Pure/ML-Systems/ml_debugger_dummy.ML	Thu Jul 16 11:38:18 2015 +0200
     2.3 @@ -6,8 +6,6 @@
     2.4  
     2.5  signature ML_DEBUGGER =
     2.6  sig
     2.7 -  type compiler_parameters
     2.8 -  val compiler_parameters: compiler_parameters
     2.9    type location
    2.10    val on_entry: (string * location -> unit) option -> unit
    2.11    val on_exit: (string * location -> unit) option -> unit
    2.12 @@ -25,12 +23,6 @@
    2.13  structure ML_Debugger: ML_DEBUGGER =
    2.14  struct
    2.15  
    2.16 -(* compiler parameters *)
    2.17 -
    2.18 -type compiler_parameters = unit;
    2.19 -val compiler_parameters = ();
    2.20 -
    2.21 -
    2.22  (* hooks *)
    2.23  
    2.24  type location = unit;
    2.25 @@ -54,3 +46,6 @@
    2.26  fun debug_name_space () = fail ();
    2.27  
    2.28  end;
    2.29 +
    2.30 +
    2.31 +fun ml_debugger_parameters (_: bool) = [];
     3.1 --- a/src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML	Thu Jul 16 11:10:57 2015 +0200
     3.2 +++ b/src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML	Thu Jul 16 11:38:18 2015 +0200
     3.3 @@ -7,12 +7,6 @@
     3.4  structure ML_Debugger: ML_DEBUGGER =
     3.5  struct
     3.6  
     3.7 -(* compiler parameters *)
     3.8 -
     3.9 -type compiler_parameters = PolyML.Compiler.compilerParameters;
    3.10 -val compiler_parameters = PolyML.Compiler.CPDebug true;
    3.11 -
    3.12 -
    3.13  (* hooks *)
    3.14  
    3.15  type location = PolyML.location;
    3.16 @@ -35,3 +29,6 @@
    3.17  val debug_name_space = PolyML.DebuggerInterface.debugNameSpace;
    3.18  
    3.19  end;
    3.20 +
    3.21 +fun ml_debugger_parameters false = []
    3.22 +  | ml_debugger_parameters true = [PolyML.Compiler.CPDebug true];
     4.1 --- a/src/Pure/ML/ml_compiler_polyml.ML	Thu Jul 16 11:10:57 2015 +0200
     4.2 +++ b/src/Pure/ML/ml_compiler_polyml.ML	Thu Jul 16 11:38:18 2015 +0200
     4.3 @@ -183,7 +183,8 @@
     4.4        PolyML.Compiler.CPFileName location_props,
     4.5        PolyML.Compiler.CPPrintDepth ML_Options.get_print_depth,
     4.6        PolyML.Compiler.CPCompilerResultFun result_fun,
     4.7 -      PolyML.Compiler.CPPrintInAlphabeticalOrder false];
     4.8 +      PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
     4.9 +     ml_debugger_parameters (ML_Options.debugger_enabled opt_context);
    4.10      val _ =
    4.11        (while not (List.null (! input_buffer)) do
    4.12          PolyML.compiler (get, parameters) ())
     5.1 --- a/src/Pure/ML/ml_options.ML	Thu Jul 16 11:10:57 2015 +0200
     5.2 +++ b/src/Pure/ML/ml_options.ML	Thu Jul 16 11:38:18 2015 +0200
     5.3 @@ -11,6 +11,9 @@
     5.4    val exception_trace_raw: Config.raw
     5.5    val exception_trace: bool Config.T
     5.6    val exception_trace_enabled: Context.generic option -> bool
     5.7 +  val debugger_raw: Config.raw
     5.8 +  val debugger: bool Config.T
     5.9 +  val debugger_enabled: Context.generic option -> bool
    5.10    val print_depth_raw: Config.raw
    5.11    val print_depth: int Config.T
    5.12    val get_print_depth: unit -> int
    5.13 @@ -37,6 +40,16 @@
    5.14    | exception_trace_enabled (SOME context) = Config.get_generic context exception_trace;
    5.15  
    5.16  
    5.17 +(* debugger *)
    5.18 +
    5.19 +val debugger_raw = Config.declare_option ("ML_debugger", @{here});
    5.20 +val debugger = Config.bool debugger_raw;
    5.21 +
    5.22 +fun debugger_enabled NONE =
    5.23 +      (Options.default_bool (Config.name_of debugger_raw) handle ERROR _ => false)
    5.24 +  | debugger_enabled (SOME context) = Config.get_generic context debugger;
    5.25 +
    5.26 +
    5.27  (* print depth *)
    5.28  
    5.29  val print_depth_raw =