merge
authorblanchet
Thu Jul 16 17:36:38 2015 +0200 (2015-07-16)
changeset 60738a2a376689082
parent 60737 685b169d0611
parent 60734 6aaa9b95cf47
child 60739 e3f52a15c6ed
merge
     1.1 --- a/etc/options	Thu Jul 16 17:25:48 2015 +0200
     1.2 +++ b/etc/options	Thu Jul 16 17:36:38 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/General/completion.ML	Thu Jul 16 17:25:48 2015 +0200
     2.2 +++ b/src/Pure/General/completion.ML	Thu Jul 16 17:36:38 2015 +0200
     2.3 @@ -10,6 +10,7 @@
     2.4    val names: Position.T -> (string * (string * string)) list -> T
     2.5    val none: T
     2.6    val make: string * Position.T -> ((string -> bool) -> (string * (string * string)) list) -> T
     2.7 +  val encode: T -> XML.body
     2.8    val reported_text: T -> string
     2.9    val suppress_abbrevs: string -> Markup.T list
    2.10  end;
    2.11 @@ -40,14 +41,18 @@
    2.12    then names pos (make_names (String.isPrefix (Name.clean name)))
    2.13    else none;
    2.14  
    2.15 +fun encode completion =
    2.16 +  let
    2.17 +    val {total, names, ...} = dest completion;
    2.18 +    open XML.Encode;
    2.19 +  in pair int (list (pair string (pair string string))) (total, names) end;
    2.20 +
    2.21  fun reported_text completion =
    2.22 -  let val {pos, total, names} = dest completion in
    2.23 +  let val {pos, names, ...} = dest completion in
    2.24      if Position.is_reported pos andalso not (null names) then
    2.25        let
    2.26          val markup = Position.markup pos Markup.completion;
    2.27 -        val body = (total, names) |>
    2.28 -          let open XML.Encode in pair int (list (pair string (pair string string))) end;
    2.29 -      in YXML.string_of (XML.Elem (markup, body)) end
    2.30 +      in YXML.string_of (XML.Elem (markup, encode completion)) end
    2.31      else ""
    2.32    end;
    2.33  
     3.1 --- a/src/Pure/General/completion.scala	Thu Jul 16 17:25:48 2015 +0200
     3.2 +++ b/src/Pure/General/completion.scala	Thu Jul 16 17:36:38 2015 +0200
     3.3 @@ -199,7 +199,8 @@
     3.4              if (kind == "") (name, quote(decode(name)))
     3.5              else
     3.6               (Long_Name.qualify(kind, name),
     3.7 -              Word.implode(Word.explode('_', kind)) + " " + quote(decode(name)))
     3.8 +              Word.implode(Word.explode('_', kind)) +
     3.9 +              (if (xname == name) "" else " " + quote(decode(name))))
    3.10            description = List(xname1, "(" + descr_name + ")")
    3.11          } yield Item(range, original, full_name, description, xname1, 0, true)
    3.12  
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/ML-Systems/ml_debugger_dummy.ML	Thu Jul 16 17:36:38 2015 +0200
     4.3 @@ -0,0 +1,51 @@
     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_break_point: (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_break_point _ = ();
    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 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML	Thu Jul 16 17:36:38 2015 +0200
     5.3 @@ -0,0 +1,34 @@
     5.4 +(*  Title:      Pure/ML/ml_debugger_polyml-5.5.3.ML
     5.5 +    Author:     Makarius
     5.6 +
     5.7 +ML debugger interface -- Poly/ML 5.5.3, or later.
     5.8 +*)
     5.9 +
    5.10 +structure ML_Debugger: ML_DEBUGGER =
    5.11 +struct
    5.12 +
    5.13 +(* hooks *)
    5.14 +
    5.15 +type location = PolyML.location;
    5.16 +
    5.17 +val on_entry = PolyML.DebuggerInterface.setOnEntry;
    5.18 +val on_exit = PolyML.DebuggerInterface.setOnExit;
    5.19 +val on_exit_exception = PolyML.DebuggerInterface.setOnExitException;
    5.20 +val on_break_point = PolyML.DebuggerInterface.setOnBreakPoint;
    5.21 +
    5.22 +
    5.23 +(* debugger operations *)
    5.24 +
    5.25 +type state = PolyML.DebuggerInterface.debugState;
    5.26 +
    5.27 +val state = PolyML.DebuggerInterface.debugState;
    5.28 +val debug_function = PolyML.DebuggerInterface.debugFunction;
    5.29 +val debug_function_arg = PolyML.DebuggerInterface.debugFunctionArg;
    5.30 +val debug_function_result = PolyML.DebuggerInterface.debugFunctionResult;
    5.31 +val debug_location = PolyML.DebuggerInterface.debugLocation;
    5.32 +val debug_name_space = PolyML.DebuggerInterface.debugNameSpace;
    5.33 +
    5.34 +end;
    5.35 +
    5.36 +fun ml_debugger_parameters false = []
    5.37 +  | ml_debugger_parameters true = [PolyML.Compiler.CPDebug true];
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Pure/ML-Systems/ml_parse_tree.ML	Thu Jul 16 17:36:38 2015 +0200
     6.3 @@ -0,0 +1,19 @@
     6.4 +(*  Title:      Pure/ML/ml_parse_tree.ML
     6.5 +    Author:     Makarius
     6.6 +
     6.7 +Additional ML parse tree components for Poly/ML.
     6.8 +*)
     6.9 +
    6.10 +signature ML_PARSE_TREE =
    6.11 +sig
    6.12 +  val completions: PolyML.ptProperties -> string list option
    6.13 +  val break_point: PolyML.ptProperties -> bool Unsynchronized.ref option
    6.14 +end;
    6.15 +
    6.16 +structure ML_Parse_Tree: ML_PARSE_TREE =
    6.17 +struct
    6.18 +
    6.19 +fun completions _ = NONE;
    6.20 +fun break_point _ = NONE;
    6.21 +
    6.22 +end;
    6.23 \ No newline at end of file
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Pure/ML-Systems/ml_parse_tree_polyml-5.5.3.ML	Thu Jul 16 17:36:38 2015 +0200
     7.3 @@ -0,0 +1,16 @@
     7.4 +(*  Title:      Pure/ML/ml_parse_tree_polyml-5.5.3.ML
     7.5 +    Author:     Makarius
     7.6 +
     7.7 +Additional ML parse tree components for Poly/ML 5.5.3, or later.
     7.8 +*)
     7.9 +
    7.10 +structure ML_Parse_Tree: ML_PARSE_TREE =
    7.11 +struct
    7.12 +
    7.13 +fun completions (PolyML.PTcompletions x) = SOME x
    7.14 +  | completions _ = NONE;
    7.15 +
    7.16 +fun break_point (PolyML.PTbreakPoint x) = SOME x
    7.17 +  | break_point _ = NONE;
    7.18 +
    7.19 +end;
    7.20 \ No newline at end of file
     8.1 --- a/src/Pure/ML-Systems/polyml.ML	Thu Jul 16 17:25:48 2015 +0200
     8.2 +++ b/src/Pure/ML-Systems/polyml.ML	Thu Jul 16 17:36:38 2015 +0200
     8.3 @@ -132,6 +132,15 @@
     8.4  
     8.5  fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
     8.6  
     8.7 +use "ML-Systems/ml_parse_tree.ML";
     8.8 +if ML_System.name = "polyml-5.5.3" then use "ML-Systems/ml_parse_tree_polyml-5.5.3.ML" else ();
     8.9 +
    8.10 +
    8.11 +(* ML debugger *)
    8.12 +
    8.13 +use "ML-Systems/ml_debugger_dummy.ML";
    8.14 +if ML_System.name = "polyml-5.5.3" then use "ML-Systems/ml_debugger_polyml-5.5.3.ML" else ();
    8.15 +
    8.16  
    8.17  (* ML toplevel pretty printing *)
    8.18  
    8.19 @@ -188,4 +197,3 @@
    8.20  fun ml_make_string struct_name =
    8.21    "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, " ^
    8.22      struct_name ^ ".ML_print_depth ())))))";
    8.23 -
     9.1 --- a/src/Pure/ML-Systems/smlnj.ML	Thu Jul 16 17:25:48 2015 +0200
     9.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Thu Jul 16 17:36:38 2015 +0200
     9.3 @@ -162,6 +162,7 @@
     9.4  
     9.5  
     9.6  use "ML-Systems/unsynchronized.ML";
     9.7 +use "ML-Systems/ml_debugger_dummy.ML";
     9.8  
     9.9  
    9.10  (* ML system operations *)
    9.11 @@ -178,4 +179,3 @@
    9.12    else OS.FileSys.rename {old = name ^ "." ^ platform, new = name};
    9.13  
    9.14  end;
    9.15 -
    10.1 --- a/src/Pure/ML/ml_compiler_polyml.ML	Thu Jul 16 17:25:48 2015 +0200
    10.2 +++ b/src/Pure/ML/ml_compiler_polyml.ML	Thu Jul 16 17:36:38 2015 +0200
    10.3 @@ -43,13 +43,26 @@
    10.4            in cons (pos, markup, fn () => "") end
    10.5        end;
    10.6  
    10.7 +    fun reported_completions loc names =
    10.8 +      let val pos = Exn_Properties.position_of loc in
    10.9 +        if is_reported pos andalso not (null names) then
   10.10 +          let
   10.11 +            val completion = Completion.names pos (map (fn a => (a, ("ML", a))) names);
   10.12 +            val xml = Completion.encode completion;
   10.13 +          in cons (pos, fn () => Markup.completion, fn () => YXML.string_of_body xml) end
   10.14 +        else I
   10.15 +      end;
   10.16 +
   10.17      fun reported loc (PolyML.PTtype types) = reported_types loc types
   10.18        | reported loc (PolyML.PTdeclaredAt decl) = reported_entity Markup.ML_defN loc decl
   10.19        | reported loc (PolyML.PTopenedAt decl) = reported_entity Markup.ML_openN loc decl
   10.20        | reported loc (PolyML.PTstructureAt decl) = reported_entity Markup.ML_structureN loc decl
   10.21        | reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
   10.22        | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
   10.23 -      | reported _ _ = I
   10.24 +      | reported loc pt =
   10.25 +          (case ML_Parse_Tree.completions pt of
   10.26 +            SOME names => reported_completions loc names
   10.27 +          | NONE => I)
   10.28      and reported_tree (loc, props) = fold (reported loc) props;
   10.29  
   10.30      val persistent_reports = reported_tree parse_tree [];
   10.31 @@ -183,7 +196,8 @@
   10.32        PolyML.Compiler.CPFileName location_props,
   10.33        PolyML.Compiler.CPPrintDepth ML_Options.get_print_depth,
   10.34        PolyML.Compiler.CPCompilerResultFun result_fun,
   10.35 -      PolyML.Compiler.CPPrintInAlphabeticalOrder false];
   10.36 +      PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
   10.37 +     ml_debugger_parameters (ML_Options.debugger_enabled opt_context);
   10.38      val _ =
   10.39        (while not (List.null (! input_buffer)) do
   10.40          PolyML.compiler (get, parameters) ())
    11.1 --- a/src/Pure/ML/ml_options.ML	Thu Jul 16 17:25:48 2015 +0200
    11.2 +++ b/src/Pure/ML/ml_options.ML	Thu Jul 16 17:36:38 2015 +0200
    11.3 @@ -11,6 +11,9 @@
    11.4    val exception_trace_raw: Config.raw
    11.5    val exception_trace: bool Config.T
    11.6    val exception_trace_enabled: Context.generic option -> bool
    11.7 +  val debugger_raw: Config.raw
    11.8 +  val debugger: bool Config.T
    11.9 +  val debugger_enabled: Context.generic option -> bool
   11.10    val print_depth_raw: Config.raw
   11.11    val print_depth: int Config.T
   11.12    val get_print_depth: unit -> int
   11.13 @@ -37,6 +40,16 @@
   11.14    | exception_trace_enabled (SOME context) = Config.get_generic context exception_trace;
   11.15  
   11.16  
   11.17 +(* debugger *)
   11.18 +
   11.19 +val debugger_raw = Config.declare_option ("ML_debugger", @{here});
   11.20 +val debugger = Config.bool debugger_raw;
   11.21 +
   11.22 +fun debugger_enabled NONE =
   11.23 +      (Options.default_bool (Config.name_of debugger_raw) handle ERROR _ => false)
   11.24 +  | debugger_enabled (SOME context) = Config.get_generic context debugger;
   11.25 +
   11.26 +
   11.27  (* print depth *)
   11.28  
   11.29  val print_depth_raw =
    12.1 --- a/src/Pure/ROOT	Thu Jul 16 17:25:48 2015 +0200
    12.2 +++ b/src/Pure/ROOT	Thu Jul 16 17:36:38 2015 +0200
    12.3 @@ -6,21 +6,25 @@
    12.4      "General/exn.ML"
    12.5      "ML-Systems/compiler_polyml.ML"
    12.6      "ML-Systems/exn_trace_polyml-5.5.1.ML"
    12.7 +    "ML-Systems/ml_debugger_dummy.ML"
    12.8 +    "ML-Systems/ml_debugger_polyml-5.5.3.ML"
    12.9      "ML-Systems/ml_name_space.ML"
   12.10 +    "ML-Systems/ml_parse_tree.ML"
   12.11 +    "ML-Systems/ml_parse_tree_polyml-5.5.3.ML"
   12.12      "ML-Systems/ml_positions.ML"
   12.13      "ML-Systems/ml_pretty.ML"
   12.14      "ML-Systems/ml_system.ML"
   12.15      "ML-Systems/multithreading.ML"
   12.16      "ML-Systems/multithreading_polyml.ML"
   12.17      "ML-Systems/overloading_smlnj.ML"
   12.18 -    "ML-Systems/polyml.ML"
   12.19      "ML-Systems/polyml-5.5.2.ML"
   12.20      "ML-Systems/polyml-5.5.3.ML"
   12.21 +    "ML-Systems/polyml.ML"
   12.22      "ML-Systems/pp_dummy.ML"
   12.23      "ML-Systems/proper_int.ML"
   12.24 +    "ML-Systems/share_common_data_polyml-5.3.0.ML"
   12.25      "ML-Systems/single_assignment.ML"
   12.26      "ML-Systems/single_assignment_polyml.ML"
   12.27 -    "ML-Systems/share_common_data_polyml-5.3.0.ML"
   12.28      "ML-Systems/smlnj.ML"
   12.29      "ML-Systems/thread_dummy.ML"
   12.30      "ML-Systems/universal.ML"
   12.31 @@ -33,18 +37,23 @@
   12.32      "General/exn.ML"
   12.33      "ML-Systems/compiler_polyml.ML"
   12.34      "ML-Systems/exn_trace_polyml-5.5.1.ML"
   12.35 +    "ML-Systems/ml_debugger_dummy.ML"
   12.36 +    "ML-Systems/ml_debugger_polyml-5.5.3.ML"
   12.37      "ML-Systems/ml_name_space.ML"
   12.38 +    "ML-Systems/ml_parse_tree.ML"
   12.39 +    "ML-Systems/ml_parse_tree_polyml-5.5.3.ML"
   12.40      "ML-Systems/ml_positions.ML"
   12.41      "ML-Systems/ml_pretty.ML"
   12.42      "ML-Systems/ml_system.ML"
   12.43      "ML-Systems/multithreading.ML"
   12.44      "ML-Systems/multithreading_polyml.ML"
   12.45      "ML-Systems/overloading_smlnj.ML"
   12.46 -    "ML-Systems/polyml.ML"
   12.47      "ML-Systems/polyml-5.5.2.ML"
   12.48      "ML-Systems/polyml-5.5.3.ML"
   12.49 +    "ML-Systems/polyml.ML"
   12.50      "ML-Systems/pp_dummy.ML"
   12.51      "ML-Systems/proper_int.ML"
   12.52 +    "ML-Systems/share_common_data_polyml-5.3.0.ML"
   12.53      "ML-Systems/single_assignment.ML"
   12.54      "ML-Systems/single_assignment_polyml.ML"
   12.55      "ML-Systems/smlnj.ML"