equal
deleted
inserted
replaced
19 val debug_function: state -> string |
19 val debug_function: state -> string |
20 val debug_function_arg: state -> ML_Name_Space.valueVal |
20 val debug_function_arg: state -> ML_Name_Space.valueVal |
21 val debug_function_result: state -> ML_Name_Space.valueVal |
21 val debug_function_result: state -> ML_Name_Space.valueVal |
22 val debug_location: state -> 'location |
22 val debug_location: state -> 'location |
23 val debug_name_space: state -> ML_Name_Space.T |
23 val debug_name_space: state -> ML_Name_Space.T |
|
24 val debug_local_name_space: state -> ML_Name_Space.T |
24 end; |
25 end; |
25 |
26 |
26 structure ML_Debugger: ML_DEBUGGER = |
27 structure ML_Debugger: ML_DEBUGGER = |
27 struct |
28 struct |
28 |
29 |
56 fun debug_function () = fail (); |
57 fun debug_function () = fail (); |
57 fun debug_function_arg () = fail (); |
58 fun debug_function_arg () = fail (); |
58 fun debug_function_result () = fail (); |
59 fun debug_function_result () = fail (); |
59 fun debug_location () = fail (); |
60 fun debug_location () = fail (); |
60 fun debug_name_space () = fail (); |
61 fun debug_name_space () = fail (); |
|
62 fun debug_local_name_space () = fail (); |
61 |
63 |
62 end; |
64 end; |