# HG changeset patch
# User wenzelm
# Date 1450709183 -3600
# Node ID 5a9a85c4cfb3e648167ab41606087e20a811aad4
# Parent  acdfc76a6c33f4b6e99b37d508dfb224aa5ed64e
tuned message;

diff -r acdfc76a6c33 -r 5a9a85c4cfb3 src/Pure/ML-Systems/ml_debugger.ML
--- a/src/Pure/ML-Systems/ml_debugger.ML	Mon Dec 21 15:09:35 2015 +0100
+++ b/src/Pure/ML-Systems/ml_debugger.ML	Mon Dec 21 15:46:23 2015 +0100
@@ -21,6 +21,7 @@
   val debug_function_result: state -> ML_Name_Space.valueVal
   val debug_location: state -> 'location
   val debug_name_space: state -> ML_Name_Space.T
+  val debug_local_name_space: state -> ML_Name_Space.T
 end;
 
 structure ML_Debugger: ML_DEBUGGER =
@@ -58,5 +59,6 @@
 fun debug_function_result () = fail ();
 fun debug_location () = fail ();
 fun debug_name_space () = fail ();
+fun debug_local_name_space () = fail ();
 
 end;
diff -r acdfc76a6c33 -r 5a9a85c4cfb3 src/Pure/ML-Systems/ml_debugger_polyml-5.6.ML
--- a/src/Pure/ML-Systems/ml_debugger_polyml-5.6.ML	Mon Dec 21 15:09:35 2015 +0100
+++ b/src/Pure/ML-Systems/ml_debugger_polyml-5.6.ML	Mon Dec 21 15:46:23 2015 +0100
@@ -22,6 +22,7 @@
   val debug_function_result: state -> ML_Name_Space.valueVal
   val debug_location: state -> location
   val debug_name_space: state -> ML_Name_Space.T
+  val debug_local_name_space: state -> ML_Name_Space.T
 end;
 
 structure ML_Debugger: ML_DEBUGGER =
@@ -66,5 +67,6 @@
 val debug_function_result = PolyML.DebuggerInterface.debugFunctionResult;
 val debug_location = PolyML.DebuggerInterface.debugLocation;
 val debug_name_space = PolyML.DebuggerInterface.debugNameSpace;
+val debug_local_name_space = PolyML.DebuggerInterface.debugLocalNameSpace;
 
 end;
diff -r acdfc76a6c33 -r 5a9a85c4cfb3 src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Mon Dec 21 15:09:35 2015 +0100
+++ b/src/Pure/Tools/debugger.ML	Mon Dec 21 15:46:23 2015 +0100
@@ -191,7 +191,7 @@
     fun print x =
       Pretty.from_ML (ML_Name_Space.display_val (x, ML_Options.get_print_depth (), space));
     fun print_all () =
-      #allVal (ML_Debugger.debug_name_space (the_debug_state thread_name index)) ()
+      #allVal (ML_Debugger.debug_local_name_space (the_debug_state thread_name index)) ()
       |> sort_by #1 |> map (Pretty.item o single o print o #2)
       |> Pretty.chunks |> Pretty.string_of |> writeln_message;
   in Context.setmp_thread_data (SOME context) print_all () end;