# HG changeset patch # User wenzelm # Date 1437057157 -7200 # Node ID 7a72429c5a1fb09a80e837f482ba56aa3eedef82 # Parent 53697011b03af96595ce90c13d2b42433ba03d70# Parent 18299765542e9ef739cbee8f4e33303c775ba2fe merged diff -r 53697011b03a -r 7a72429c5a1f etc/options --- a/etc/options Thu Jul 16 10:48:20 2015 +0200 +++ b/etc/options Thu Jul 16 16:32:37 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" diff -r 53697011b03a -r 7a72429c5a1f src/Pure/General/completion.ML --- a/src/Pure/General/completion.ML Thu Jul 16 10:48:20 2015 +0200 +++ b/src/Pure/General/completion.ML Thu Jul 16 16:32:37 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; diff -r 53697011b03a -r 7a72429c5a1f src/Pure/General/completion.scala --- a/src/Pure/General/completion.scala Thu Jul 16 10:48:20 2015 +0200 +++ b/src/Pure/General/completion.scala Thu Jul 16 16:32:37 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) diff -r 53697011b03a -r 7a72429c5a1f src/Pure/ML-Systems/ml_debugger_dummy.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML-Systems/ml_debugger_dummy.ML Thu Jul 16 16:32:37 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) = []; diff -r 53697011b03a -r 7a72429c5a1f src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML --- /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 16:32:37 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]; diff -r 53697011b03a -r 7a72429c5a1f src/Pure/ML-Systems/ml_parse_tree.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML-Systems/ml_parse_tree.ML Thu Jul 16 16:32:37 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 diff -r 53697011b03a -r 7a72429c5a1f src/Pure/ML-Systems/ml_parse_tree_polyml-5.5.3.ML --- /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 16:32:37 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 diff -r 53697011b03a -r 7a72429c5a1f src/Pure/ML-Systems/polyml.ML --- a/src/Pure/ML-Systems/polyml.ML Thu Jul 16 10:48:20 2015 +0200 +++ b/src/Pure/ML-Systems/polyml.ML Thu Jul 16 16:32:37 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 ())))))"; - diff -r 53697011b03a -r 7a72429c5a1f src/Pure/ML-Systems/smlnj.ML --- a/src/Pure/ML-Systems/smlnj.ML Thu Jul 16 10:48:20 2015 +0200 +++ b/src/Pure/ML-Systems/smlnj.ML Thu Jul 16 16:32:37 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; - diff -r 53697011b03a -r 7a72429c5a1f src/Pure/ML/ml_compiler_polyml.ML --- a/src/Pure/ML/ml_compiler_polyml.ML Thu Jul 16 10:48:20 2015 +0200 +++ b/src/Pure/ML/ml_compiler_polyml.ML Thu Jul 16 16:32:37 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) ()) diff -r 53697011b03a -r 7a72429c5a1f src/Pure/ML/ml_options.ML --- a/src/Pure/ML/ml_options.ML Thu Jul 16 10:48:20 2015 +0200 +++ b/src/Pure/ML/ml_options.ML Thu Jul 16 16:32:37 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 = diff -r 53697011b03a -r 7a72429c5a1f src/Pure/ROOT --- a/src/Pure/ROOT Thu Jul 16 10:48:20 2015 +0200 +++ b/src/Pure/ROOT Thu Jul 16 16:32:37 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"