# HG changeset patch
# User wenzelm
# Date 1438854407 -7200
# Node ID 1c51a2ca820452f2beb91869e362a6da6c2ea037
# Parent  35932863b1143a6bf833f2f02c80f95b24531571
clarified signature, to make debugger.ML compile with current official ML versions;

diff -r 35932863b114 -r 1c51a2ca8204 src/Pure/ML-Systems/ml_debugger.ML
--- a/src/Pure/ML-Systems/ml_debugger.ML	Wed Aug 05 21:46:52 2015 +0200
+++ b/src/Pure/ML-Systems/ml_debugger.ML	Thu Aug 06 11:46:47 2015 +0200
@@ -6,17 +6,16 @@
 
 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_breakpoint: (location * bool Unsynchronized.ref -> unit) option -> unit
+  val on_entry: (string * 'a -> unit) option -> unit
+  val on_exit: (string * 'a -> unit) option -> unit
+  val on_exit_exception: (string * 'a -> exn -> unit) option -> unit
+  val on_breakpoint: ('a * 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_location: state -> 'a
   val debug_name_space: state -> ML_Name_Space.T
 end;
 
diff -r 35932863b114 -r 1c51a2ca8204 src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML
--- a/src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML	Wed Aug 05 21:46:52 2015 +0200
+++ b/src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML	Thu Aug 06 11:46:47 2015 +0200
@@ -4,6 +4,22 @@
 ML debugger interface -- Poly/ML 5.5.3, or later.
 *)
 
+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_breakpoint: (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