merged
authorwenzelm
Thu, 16 Jul 2015 17:02:07 +0200
changeset 60737 6aaa9b95cf47
parent 60728 26ffdb966759 (current diff)
parent 60736 7a72429c5a1f (diff)
child 60738 a2a376689082
merged
--- 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"