--- a/etc/options Thu Jul 16 12:23:22 2015 +0200
+++ b/etc/options Thu Jul 16 17:02:07 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/General/completion.ML Thu Jul 16 12:23:22 2015 +0200
+++ b/src/Pure/General/completion.ML Thu Jul 16 17:02:07 2015 +0200
@@ -10,6 +10,7 @@
val names: Position.T -> (string * (string * string)) list -> T
val none: T
val make: string * Position.T -> ((string -> bool) -> (string * (string * string)) list) -> T
+ val encode: T -> XML.body
val reported_text: T -> string
val suppress_abbrevs: string -> Markup.T list
end;
@@ -40,14 +41,18 @@
then names pos (make_names (String.isPrefix (Name.clean name)))
else none;
+fun encode completion =
+ let
+ val {total, names, ...} = dest completion;
+ open XML.Encode;
+ in pair int (list (pair string (pair string string))) (total, names) end;
+
fun reported_text completion =
- let val {pos, total, names} = dest completion in
+ let val {pos, names, ...} = dest completion in
if Position.is_reported pos andalso not (null names) then
let
val markup = Position.markup pos Markup.completion;
- val body = (total, names) |>
- let open XML.Encode in pair int (list (pair string (pair string string))) end;
- in YXML.string_of (XML.Elem (markup, body)) end
+ in YXML.string_of (XML.Elem (markup, encode completion)) end
else ""
end;
--- a/src/Pure/General/completion.scala Thu Jul 16 12:23:22 2015 +0200
+++ b/src/Pure/General/completion.scala Thu Jul 16 17:02:07 2015 +0200
@@ -199,7 +199,8 @@
if (kind == "") (name, quote(decode(name)))
else
(Long_Name.qualify(kind, name),
- Word.implode(Word.explode('_', kind)) + " " + quote(decode(name)))
+ Word.implode(Word.explode('_', kind)) +
+ (if (xname == name) "" else " " + quote(decode(name))))
description = List(xname1, "(" + descr_name + ")")
} yield Item(range, original, full_name, description, xname1, 0, true)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/ml_debugger_dummy.ML Thu Jul 16 17:02:07 2015 +0200
@@ -0,0 +1,51 @@
+(* 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_break_point: (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_break_point _ = ();
+
+
+(* 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) = [];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML Thu Jul 16 17:02:07 2015 +0200
@@ -0,0 +1,34 @@
+(* Title: Pure/ML/ml_debugger_polyml-5.5.3.ML
+ Author: Makarius
+
+ML debugger interface -- Poly/ML 5.5.3, or later.
+*)
+
+structure ML_Debugger: ML_DEBUGGER =
+struct
+
+(* hooks *)
+
+type location = PolyML.location;
+
+val on_entry = PolyML.DebuggerInterface.setOnEntry;
+val on_exit = PolyML.DebuggerInterface.setOnExit;
+val on_exit_exception = PolyML.DebuggerInterface.setOnExitException;
+val on_break_point = PolyML.DebuggerInterface.setOnBreakPoint;
+
+
+(* debugger operations *)
+
+type state = PolyML.DebuggerInterface.debugState;
+
+val state = PolyML.DebuggerInterface.debugState;
+val debug_function = PolyML.DebuggerInterface.debugFunction;
+val debug_function_arg = PolyML.DebuggerInterface.debugFunctionArg;
+val debug_function_result = PolyML.DebuggerInterface.debugFunctionResult;
+val debug_location = PolyML.DebuggerInterface.debugLocation;
+val debug_name_space = PolyML.DebuggerInterface.debugNameSpace;
+
+end;
+
+fun ml_debugger_parameters false = []
+ | ml_debugger_parameters true = [PolyML.Compiler.CPDebug true];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/ml_parse_tree.ML Thu Jul 16 17:02:07 2015 +0200
@@ -0,0 +1,19 @@
+(* Title: Pure/ML/ml_parse_tree.ML
+ Author: Makarius
+
+Additional ML parse tree components for Poly/ML.
+*)
+
+signature ML_PARSE_TREE =
+sig
+ val completions: PolyML.ptProperties -> string list option
+ val break_point: PolyML.ptProperties -> bool Unsynchronized.ref option
+end;
+
+structure ML_Parse_Tree: ML_PARSE_TREE =
+struct
+
+fun completions _ = NONE;
+fun break_point _ = NONE;
+
+end;
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/ml_parse_tree_polyml-5.5.3.ML Thu Jul 16 17:02:07 2015 +0200
@@ -0,0 +1,16 @@
+(* Title: Pure/ML/ml_parse_tree_polyml-5.5.3.ML
+ Author: Makarius
+
+Additional ML parse tree components for Poly/ML 5.5.3, or later.
+*)
+
+structure ML_Parse_Tree: ML_PARSE_TREE =
+struct
+
+fun completions (PolyML.PTcompletions x) = SOME x
+ | completions _ = NONE;
+
+fun break_point (PolyML.PTbreakPoint x) = SOME x
+ | break_point _ = NONE;
+
+end;
\ No newline at end of file
--- a/src/Pure/ML-Systems/polyml.ML Thu Jul 16 12:23:22 2015 +0200
+++ b/src/Pure/ML-Systems/polyml.ML Thu Jul 16 17:02:07 2015 +0200
@@ -132,6 +132,15 @@
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 ();
+
+
+(* ML debugger *)
+
+use "ML-Systems/ml_debugger_dummy.ML";
+if ML_System.name = "polyml-5.5.3" then use "ML-Systems/ml_debugger_polyml-5.5.3.ML" else ();
+
(* ML toplevel pretty printing *)
@@ -188,4 +197,3 @@
fun ml_make_string struct_name =
"(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, " ^
struct_name ^ ".ML_print_depth ())))))";
-
--- a/src/Pure/ML-Systems/smlnj.ML Thu Jul 16 12:23:22 2015 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML Thu Jul 16 17:02:07 2015 +0200
@@ -162,6 +162,7 @@
use "ML-Systems/unsynchronized.ML";
+use "ML-Systems/ml_debugger_dummy.ML";
(* ML system operations *)
@@ -178,4 +179,3 @@
else OS.FileSys.rename {old = name ^ "." ^ platform, new = name};
end;
-
--- a/src/Pure/ML/ml_compiler_polyml.ML Thu Jul 16 12:23:22 2015 +0200
+++ b/src/Pure/ML/ml_compiler_polyml.ML Thu Jul 16 17:02:07 2015 +0200
@@ -43,13 +43,26 @@
in cons (pos, markup, fn () => "") end
end;
+ fun reported_completions loc names =
+ let val pos = Exn_Properties.position_of loc in
+ if is_reported pos andalso not (null names) then
+ let
+ val completion = Completion.names pos (map (fn a => (a, ("ML", a))) names);
+ val xml = Completion.encode completion;
+ in cons (pos, fn () => Markup.completion, fn () => YXML.string_of_body xml) end
+ else I
+ end;
+
fun reported loc (PolyML.PTtype types) = reported_types loc types
| reported loc (PolyML.PTdeclaredAt decl) = reported_entity Markup.ML_defN loc decl
| reported loc (PolyML.PTopenedAt decl) = reported_entity Markup.ML_openN loc decl
| reported loc (PolyML.PTstructureAt decl) = reported_entity Markup.ML_structureN loc decl
| reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
| reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
- | reported _ _ = I
+ | reported loc pt =
+ (case ML_Parse_Tree.completions pt of
+ SOME names => reported_completions loc names
+ | NONE => I)
and reported_tree (loc, props) = fold (reported loc) props;
val persistent_reports = reported_tree parse_tree [];
@@ -183,7 +196,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 12:23:22 2015 +0200
+++ b/src/Pure/ML/ml_options.ML Thu Jul 16 17:02:07 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 =
--- a/src/Pure/ROOT Thu Jul 16 12:23:22 2015 +0200
+++ b/src/Pure/ROOT Thu Jul 16 17:02:07 2015 +0200
@@ -6,21 +6,25 @@
"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_debugger_polyml-5.5.3.ML"
"ML-Systems/ml_name_space.ML"
+ "ML-Systems/ml_parse_tree.ML"
+ "ML-Systems/ml_parse_tree_polyml-5.5.3.ML"
"ML-Systems/ml_positions.ML"
"ML-Systems/ml_pretty.ML"
"ML-Systems/ml_system.ML"
"ML-Systems/multithreading.ML"
"ML-Systems/multithreading_polyml.ML"
"ML-Systems/overloading_smlnj.ML"
- "ML-Systems/polyml.ML"
"ML-Systems/polyml-5.5.2.ML"
"ML-Systems/polyml-5.5.3.ML"
+ "ML-Systems/polyml.ML"
"ML-Systems/pp_dummy.ML"
"ML-Systems/proper_int.ML"
+ "ML-Systems/share_common_data_polyml-5.3.0.ML"
"ML-Systems/single_assignment.ML"
"ML-Systems/single_assignment_polyml.ML"
- "ML-Systems/share_common_data_polyml-5.3.0.ML"
"ML-Systems/smlnj.ML"
"ML-Systems/thread_dummy.ML"
"ML-Systems/universal.ML"
@@ -33,18 +37,23 @@
"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_debugger_polyml-5.5.3.ML"
"ML-Systems/ml_name_space.ML"
+ "ML-Systems/ml_parse_tree.ML"
+ "ML-Systems/ml_parse_tree_polyml-5.5.3.ML"
"ML-Systems/ml_positions.ML"
"ML-Systems/ml_pretty.ML"
"ML-Systems/ml_system.ML"
"ML-Systems/multithreading.ML"
"ML-Systems/multithreading_polyml.ML"
"ML-Systems/overloading_smlnj.ML"
- "ML-Systems/polyml.ML"
"ML-Systems/polyml-5.5.2.ML"
"ML-Systems/polyml-5.5.3.ML"
+ "ML-Systems/polyml.ML"
"ML-Systems/pp_dummy.ML"
"ML-Systems/proper_int.ML"
+ "ML-Systems/share_common_data_polyml-5.3.0.ML"
"ML-Systems/single_assignment.ML"
"ML-Systems/single_assignment_polyml.ML"
"ML-Systems/smlnj.ML"