--- 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;
--- 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;
--- 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;