# HG changeset patch
# User wenzelm
# Date 1437037857 -7200
# Node ID f5989a2c1f67bd717289d73219a877032f93a04b
# Parent  6d500a224cbe941068bfb92e501dd5ee4f709689
ML debugger interface;

diff -r 6d500a224cbe -r f5989a2c1f67 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 11:10:57 2015 +0200
@@ -0,0 +1,56 @@
+(*  Title:      Pure/ML/ml_debugger_dummy.ML
+    Author:     Makarius
+
+ML debugger interface -- dummy version.
+*)
+
+signature ML_DEBUGGER =
+sig
+  type compiler_parameters
+  val compiler_parameters: compiler_parameters
+  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
+
+(* compiler parameters *)
+
+type compiler_parameters = unit;
+val compiler_parameters = ();
+
+
+(* 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;
diff -r 6d500a224cbe -r f5989a2c1f67 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 11:10:57 2015 +0200
@@ -0,0 +1,37 @@
+(*  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
+
+(* compiler parameters *)
+
+type compiler_parameters = PolyML.Compiler.compilerParameters;
+val compiler_parameters = PolyML.Compiler.CPDebug true;
+
+
+(* 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;
diff -r 6d500a224cbe -r f5989a2c1f67 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Wed Jul 15 11:25:51 2015 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Thu Jul 16 11:10:57 2015 +0200
@@ -133,6 +133,12 @@
 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
 
 
+(* 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 *)
 
 use "ML-Systems/ml_pretty.ML";
@@ -188,4 +194,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 6d500a224cbe -r f5989a2c1f67 src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Wed Jul 15 11:25:51 2015 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Thu Jul 16 11:10:57 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 6d500a224cbe -r f5989a2c1f67 src/Pure/ROOT
--- a/src/Pure/ROOT	Wed Jul 15 11:25:51 2015 +0200
+++ b/src/Pure/ROOT	Thu Jul 16 11:10:57 2015 +0200
@@ -6,6 +6,8 @@
     "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_positions.ML"
     "ML-Systems/ml_pretty.ML"