# HG changeset patch
# User wenzelm
# Date 1438863839 -7200
# Node ID b0627cb2e08d10d4a54a4d45f7d7574c8414147f
# Parent  1c51a2ca820452f2beb91869e362a6da6c2ea037
tuned;

diff -r 1c51a2ca8204 -r b0627cb2e08d src/Pure/ML-Systems/ml_debugger.ML
--- a/src/Pure/ML-Systems/ml_debugger.ML	Thu Aug 06 11:46:47 2015 +0200
+++ b/src/Pure/ML-Systems/ml_debugger.ML	Thu Aug 06 14:23:59 2015 +0200
@@ -1,21 +1,21 @@
 (*  Title:      Pure/ML/ml_debugger.ML
     Author:     Makarius
 
-ML debugger interface.
+ML debugger interface -- dummy version.
 *)
 
 signature ML_DEBUGGER =
 sig
-  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
+  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 -> 'a
+  val debug_location: state -> 'location
   val debug_name_space: state -> ML_Name_Space.T
 end;
 
@@ -24,7 +24,6 @@
 
 (* hooks *)
 
-type location = unit;
 fun on_entry _ = ();
 fun on_exit _ = ();
 fun on_exit_exception _ = ();
diff -r 1c51a2ca8204 -r b0627cb2e08d src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML
--- a/src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML	Thu Aug 06 11:46:47 2015 +0200
+++ b/src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML	Thu Aug 06 14:23:59 2015 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/ML/ml_debugger_polyml-5.5.3.ML
     Author:     Makarius
 
-ML debugger interface -- Poly/ML 5.5.3, or later.
+ML debugger interface -- for Poly/ML 5.5.3, or later.
 *)
 
 signature ML_DEBUGGER =